Abstract is missing.
- Formal methods in cell BiologyJasmin Fisher. 1 [doi]
- Answer Set ProgrammingTorsten Schaub. 2 [doi]
- Formal methods for aerospace applicationsEric Feron. 3 [doi]
- Application of SMT solvers to hybrid system verificationAlessandro Cimatti. 4 [doi]
- Algebra of concurrent designTony Hoare. 5 [doi]
- Efficient predictive analysis for detecting nondeterminism in multi-threaded programsArnab Sinha, Sharad Malik, Aarti Gupta. 6-15 [doi]
- Automatic lock insertion in concurrent programsVineet Kahlon. 16-23 [doi]
- Multi-pushdown systems with budgetsParosh Aziz Abdulla, Mohamed Faouzi Atig, Othmane Rezine, Jari Stenman. 24-33 [doi]
- Quantifier elimination by Dependency SequentsEugene Goldberg, Panagiotis Manolios. 34-43 [doi]
- Preprocessing techniques for first-order clausificationKrystof Hoder, Zurab Khasidashvili, Konstantin Korovin, Andrei Voronkov. 44-51 [doi]
- A liveness checking algorithm that countsKoen Claessen, Niklas Sörensson. 52-59 [doi]
- A formal model of a large memory that supports efficient executionWarren A. Hunt Jr., Matt Kaufmann. 60-67 [doi]
- Verification with small and short worldsRohit Sinha, Cynthia Sturton, Petros Maniatis, Sanjit A. Seshia, David Wagner. 68-77 [doi]
- Decompilation into logic - ImprovedMagnus O. Myreen, Michael J. C. Gordon, Konrad Slind. 78-81 [doi]
- Complete and effective robustness checking by means of interpolationStefan Frehse, Görschwin Fey, Eli Arbel, Karen Yorav, Rolf Drechsler. 82-90 [doi]
- Symbolically synthesizing small circuitsRüdiger Ehlers, Robert Könighofer, Georg Hofferek. 91-100 [doi]
- Automated debugging of missing input constraints in a formal verification environmentBrian Keng, Andreas G. Veneris. 101-105 [doi]
- Algorithms for software model checking: Predicate abstraction vs. ImpactDirk Beyer, Philipp Wendler. 106-113 [doi]
- Incremental upgrade checking by means of interpolation-based function summariesOndrej Sery, Grigory Fedyukovich, Natasha Sharygina. 114-121 [doi]
- Verification of parametric system designsAlessandro Cimatti, Iman Narasamdya, Marco Roveri. 122-130 [doi]
- Deciding floating-point logic with systematic abstractionLeopold Haller, Alberto Griggio, Martin Brain, Daniel Kroening. 131-140 [doi]
- Formal verification of error correcting circuits using computational algebraic geometryAlexey Lvov, Luis Alfonso Lastras-Montano, Viresh Paruthi, Robert Shadowen, Ali El-Zein. 141-148 [doi]
- Symbolic Trajectory Evaluation: The primary validation Vehicle for next generation Intel® Processor Graphics FPUV. M. Achutha KiranKumar, Aarti Gupta, Rajnish Ghughal. 149-156 [doi]
- Enhanced reachability analysis via automated dynamic netlist-based hint generationJiazhao Xu, Mark Williams, Hari Mony, Jason Baumgartner. 157-164 [doi]
- Oscillator verification with probability oneChao Yan, Mark R. Greenstreet. 165-172 [doi]
- Lazy abstraction and SAT-based reachability in hardware model checkingYakir Vizel, Orna Grumberg, Sharon Shoham. 173-181 [doi]
- IC3-guided abstractionJason Baumgartner, Alexander Ivrii, Arie Matsliah, Hari Mony. 182-185 [doi]
- Formal for everyone - Challenges in achievable multicore design and verificationDaryl Stewart. 186 [doi]
- A quantifier-free SMT encoding of non-linear hybrid automataAlessandro Cimatti, Sergio Mover, Stefano Tonetta. 187-195 [doi]
- Piecewise linear modeling of nonlinear devices for formal verification of analog circuitsYan Zhang, Sriram Sankaranarayanan, Fabio Somenzi. 196-203 [doi]
- Forward and backward: Bounded model checking of linear hybrid automata from two directionsYang Yang, Lei Bu, Xuandong Li. 204-208 [doi]