Abstract is missing.
- Model Checking: Progress and ProblemsE. Allen Emerson. 1 [doi]
- Model Checking Concurrent ProgramsAarti Gupta. 2 [doi]
- Thread-Modular Shape AnalysisMooly Sagiv. 3 [doi]
- Advances in Program Termination and LivenessByron Cook. 4 [doi]
- Verification of Security ProtocolsVéronique Cortier. 5-13 [doi]
- Towards Automatic Stability Analysis for Rely-Guarantee ProofsHasan Amjad, Richard Bornat. 14-28 [doi]
- Mostly-Functional Behavior in Java ProgramsWilliam C. Benton, Charles N. Fischer. 29-43 [doi]
- The Higher-Order Aggregate Update ProblemChristos Dimoulas, Mitchell Wand. 44-58 [doi]
- An Abort-Aware Model of Transactional ProgrammingKousha Etessami, Patrice Godefroid. 59-73 [doi]
- Model-Checking the Linux Virtual File SystemAndy Galloway, Gerald Lüttgen, Jan Tobias Mühlberg, Radu Siminiceanu. 74-88 [doi]
- LTL Generalized Model Checking RevisitedPatrice Godefroid, Nir Piterman. 89-104 [doi]
- Monitoring the Full Range of omega-Regular Properties of Stochastic SystemsKalpana Gondi, Yogeshkumar Patel, A. Prasad Sistla. 105-119 [doi]
- Constraint-Based Invariant Inference over Predicate AbstractionSumit Gulwani, Saurabh Srivastava, Ramarathnam Venkatesan. 120-135 [doi]
- Reducing Behavioural to Structural Properties of Programs with ProceduresDilian Gurov, Marieke Huisman. 136-150 [doi]
- Query-Driven Program TestingAndreas Holzer, Christian Schallhart, Michael Tautschnig, Helmut Veith. 151-166 [doi]
- Average-Price-per-Reward Games on Hybrid Automata with Strong ResetsMarcin Jurdzinski, Ranko Lazic, Michal Rutkowski. 167-181 [doi]
- Abstraction Refinement for Probabilistic SoftwareMark Kattenbelt, Marta Z. Kwiatkowska, Gethin J. Norman, David Parker. 182-197 [doi]
- Finding Concurrency-Related Bugs Using Random IsolationNicholas Kidd, Thomas W. Reps, Julian Dolby, Mandana Vaziri. 198-213 [doi]
- An Abstract Interpretation-Based Framework for Control Flow Reconstruction from BinariesJohannes Kinder, Florian Zuleger, Helmut Veith. 214-228 [doi]
- SubPolyhedra: A (More) Scalable Approach to Infer Linear InequalitiesVincent Laviron, Francesco Logozzo. 229-244 [doi]
- Deciding Extensions of the Theories of Vectors and BagsPatrick Maier. 245-259 [doi]
- A PosterioriSoundness for Non-deterministic Abstract InterpretationsMatthew Might, Panagiotis Manolios. 260-274 [doi]
- An Automata-Theoretic Dynamic Completeness Criterion for Bounded Model-CheckingRotem Oshman. 275-289 [doi]
- A Scalable Memory Model for Low-Level CodeZvonimir Rakamaric, Alan J. Hu. 290-304 [doi]
- Synthesizing Switching Logic Using Constraint SolvingAnkur Taly, Sumit Gulwani, Ashish Tiwari. 305-319 [doi]
- Extending Symmetry Reduction by Exploiting System ArchitectureRichard J. Trefler, Thomas Wahl. 320-334 [doi]
- Shape-Value Abstraction for Verifying LinearizabilityViktor Vafeiadis. 335-348 [doi]
- Mixed Transition Systems RevisitedOu Wei, Arie Gurfinkel, Marsha Chechik. 349-365 [doi]
- Counterexample Generation for Discrete-Time Markov Chains Using Bounded Model CheckingRalf Wimmer, Bettina Braitling, Bernd Becker. 366-380 [doi]