Abstract is missing.
- Revisiting Positive EqualityShuvendu K. Lahiri, Randal E. Bryant, Amit Goel, Muralidhar Talupur. 1-15 [doi]
- An Interpolating Theorem ProverKenneth L. McMillan. 16-30 [doi]
- Minimal Assignments for Bounded Model CheckingKavita Ravi, Fabio Somenzi. 31-45 [doi]
- Numerical vs. Statistical Probabilistic Model Checking: An Empirical StudyHåkan L. S. Younes, Marta Z. Kwiatkowska, Gethin J. Norman, David Parker. 46-60 [doi]
- Efficient Computation of Time-Bounded Reachability Probabilities in Uniform Continuous-Time Markov Decision ProcessesChristel Baier, Boudewijn R. Haverkort, Holger Hermanns, Joost-Pieter Katoen. 61-76 [doi]
- Model Checking Discounted Temporal PropertiesLuca de Alfaro, Marco Faella, Thomas A. Henzinger, Rupak Majumdar, Mariëlle Stoelinga. 77-92 [doi]
- Automatic Creation of Environment Models via TrainingThomas Ball, Vladimir Levin, Fei Xie. 93-107 [doi]
- Error Explanation with Distance MetricsAlex Groce. 108-122 [doi]
- Online Efficient Predictive Safety Analysis of Multithreaded ProgramsKoushik Sen, Grigore Rosu, Gul Agha. 123-138 [doi]
- Vooduu: Verification of Object-Oriented Designs Using UPPAALKarsten Diethers, Michaela Huhn. 139-143 [doi]
- CoPS - Checker of Persistent SecurityCarla Piazza, Enrico Pivato, Sabina Rossi. 144-152 [doi]
- Tampere Verification ToolHeikki Virtanen, Henri Hansen, Antti Valmari, Juha Nieminen, Timo Erkkilä. 153-157 [doi]
- SyncGen: An Aspect-Oriented Framework for SynchronizationXianghua Deng, Matthew B. Dwyer, John Hatcliff, Masaaki Mizuno. 158-162 [doi]
- MetaGame: An Animation Tool for Model-Checking GamesMarkus Müller-Olm, Haiseung Yoo. 163-167 [doi]
- A Tool for Checking ANSI-C ProgramsEdmund M. Clarke, Daniel Kroening, Flavio Lerda. 168-176 [doi]
- Obtaining Memory-Efficient Reachability Graph Representations Using the Sweep-Line MethodThomas Mailund, Michael Westergaard. 177-191 [doi]
- Automated Generation of a Progress Measure for the Sweep-Line MethodKarsten Schmidt 0004. 192-204 [doi]
- Tarjan s Algorithm Makes On-the-Fly LTL Verification More EfficientJaco Geldenhuys, Antti Valmari. 205-219 [doi]
- Resource-Optimal Scheduling Using Priced Timed AutomataJacob Illum Rasmussen, Kim Guldstrand Larsen, K. Subramani. 220-235 [doi]
- Decidable and Undecidable Problems in Schedulability Analysis Using Timed AutomataPavel Krcál, Wang Yi. 236-250 [doi]
- The Succinct Solver SuiteFlemming Nielson, Hanne Riis Nielson, Hongyan Sun, Mikael Buchholtz, René Rydhof Hansen, Henrik Pilegaard, Helmut Seidl. 251-265 [doi]
- Binding-Time Analysis for MetaML via Type Inference and Constraint SolvingNathan Linger, Tim Sheard. 266-279 [doi]
- A Class of Polynomially Solvable Range Constraints for Interval Analysis without Widenings and NarrowingsZhendong Su, David Wagner. 280-295 [doi]
- A Partial Order Semantics Approach to the Clock Explosion Problem of Timed AutomataDenis Lugiez, Peter Niebert, Sarah Zennou. 296-311 [doi]
- Lower and Upper Bounds in Zone Based Abstractions of Timed AutomataGerd Behrmann, Patricia Bouyer, Kim Guldstrand Larsen, Radek Pelánek. 312-326 [doi]
- A Scalable Incomplete Test for the Boundedness of UML RT ModelsStefan Leue, Richard Mayr, Wei Wei. 327-341 [doi]
- Automatic Verification of Time Sensitive Cryptographic ProtocolsGiorgio Delzanno, Pierre Ganty. 342-356 [doi]
- Simulation-Based Verification of Autonomous Controllers via Livingstone PathFinderA. E. Lindsey, Charles Pecheur. 357-371 [doi]
- Automatic Parametric Verification of a Root Contention Protocol Based on Abstract State Machines and First Order Timed LogicDanièle Beauquier, Tristan Crolard, Evguenia Prokofieva. 372-387 [doi]
- Refining Approximations in Software Predicate AbstractionThomas Ball, Byron Cook, Satyaki Das, Sriram K. Rajamani. 388-403 [doi]
- Checking Strong Specifications Using an Extensible Software Model Checking FrameworkRobby, Edwin Rodríguez, Matthew B. Dwyer, John Hatcliff. 404-420 [doi]
- Applying Game Semantics to Compositional Software Modeling and VerificationSamson Abramsky, Dan R. Ghica, Andrzej S. Murawski, C.-H. Luke Ong. 421-435 [doi]
- Solving Disjunctive/Conjunctive Boolean Equation Systems with Alternating Fixed PointsJan Friso Groote, Misa Keinänen. 436-450 [doi]
- How Vacuous Is Vacuous?Arie Gurfinkel, Marsha Chechik. 451-466 [doi]
- A Temporal Logic of Nested Calls and ReturnsRajeev Alur, Kousha Etessami, P. Madhusudan. 467-481 [doi]
- Liveness with Incomprehensible RankingYi Fang, Nir Piterman, Amir Pnueli, Lenore D. Zuck. 482-496 [doi]
- Guided Invariant Model Checking Based on Abstraction and Symbolic Pattern DatabasesKairong Qian, Albert Nymeyer. 497-511 [doi]
- Numeric Domains with Summarized DimensionsDenis Gopan, Frank DiMaio, Nurit Dor, Thomas W. Reps, Shmuel Sagiv. 512-529 [doi]
- Symbolically Computing Most-Precise Abstract Operations for Shape AnalysisGreta Yorsh, Thomas W. Reps, Shmuel Sagiv. 530-545 [doi]
- Monotonic Abstraction-Refinement for CTLSharon Shoham, Orna Grumberg. 546-560 [doi]
- Omega-Regular Model CheckingBernard Boigelot, Axel Legay, Pierre Wolper. 561-575 [doi]
- FASTer Acceleration of Counter Automata in PracticeSébastien Bardin, Alain Finkel, Jérôme Leroux. 576-590 [doi]
- From Complementation to CertificationOrna Kupferman, Moshe Y. Vardi. 591-606 [doi]