Abstract is missing.
- Weighted Pushdown Systems and Trust-Management SystemsSomesh Jha, Stefan Schwoon, Hao Wang, Thomas W. Reps. 1-26 [doi]
- Automatic Verification of Parameterized Data StructuresJyotirmoy V. Deshmukh, E. Allen Emerson, Prateek Gupta. 27-41 [doi]
- Parameterized Verification of pi-Calculus SystemsPing Yang, Samik Basu, C. R. Ramakrishnan. 42-57 [doi]
- Easy Parameterized Verification of Biphase Mark and 8N1 ProtocolsGeoffrey M. Brown, Lee Pike. 58-72 [doi]
- Evaluating the Effectiveness of Slicing for Model Reduction of Concurrent Object-Oriented ProgramsMatthew B. Dwyer, John Hatcliff, Matthew Hoosier, Venkatesh Prasad Ranganath, Robby, Todd Wallentine. 73-89 [doi]
- New Metrics for Static Variable Ordering in Decision DiagramsRadu Siminiceanu, Gianfranco Ciardo. 90-104 [doi]
- Widening ROBDDs with Prime ImplicantsNeil Kettle, Andy King, Tadeusz Strzemecki. 105-119 [doi]
- Efficient Guided Symbolic Reachability Using Reachability ExpressionsDina Thomas, Supratik Chakraborty, Paritosh K. Pandya. 120-134 [doi]
- ::::SDSAT::::: Tight Integration of ::::Small Domain Encoding:::: and ::::Lazy:::: Approaches in a Separation Logic SolverMalay K. Ganai, Muralidhar Talupur, Aarti Gupta. 135-150 [doi]
- SAT-Based Software CertificationSagar Chaki. 151-166 [doi]
- Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof AssistantsPascal Fontaine, Jean-Yves Marion, Stephan Merz, Leonor Prensa Nieto, Alwen Fernanto Tiu. 167-181 [doi]
- Exploration of the Capabilities of Constraint Programming for Software VerificationHélène Collavizza, Michel Rueher. 182-196 [doi]
- Counterexample-Guided Abstraction Refinement for the Analysis of Graph Transformation SystemsBarbara König, Vitali Kozioura. 197-211 [doi]
- Why Waste a Perfectly Good Abstraction?Arie Gurfinkel, Marsha Chechik. 212-226 [doi]
- Efficient Abstraction Refinement in Interpolation-Based Unbounded Model CheckingBing Li, Fabio Somenzi. 227-241 [doi]
- Approximating Predicate Images for Bit-Vector LogicDaniel Kroening, Natasha Sharygina. 242-256 [doi]
- Finitary Winning in omega-Regular GamesKrishnendu Chatterjee, Thomas A. Henzinger. 257-271 [doi]
- Efficient Model Checking for LTL with Partial Order SnapshotsPeter Niebert, Doron Peled. 272-286 [doi]
- A Local Shape Analysis Based on Separation LogicDino Distefano, Peter W. O Hearn, Hongseok Yang. 287-302 [doi]
- Compositional Model Extraction for Higher-Order Concurrent ProgramsDan R. Ghica, Andrzej S. Murawski. 303-317 [doi]
- A Region Graph Based Approach to Termination ProofsStefan Leue, Wei Wei. 318-333 [doi]
- Verifying Concurrent Message-Passing C Programs with Recursive CallsSagar Chaki, Edmund M. Clarke, Nicholas Kidd, Thomas W. Reps, Tayssir Touili. 334-349 [doi]
- Automata-Based Verification of Programs with Tree UpdatesPeter Habermehl, Radu Iosif, Tomás Vojnar. 350-364 [doi]
- An Experimental Comparison of the Effectiveness of Control Flow Based Testing Approaches on Seeded FaultsAtul Gupta, Pankaj Jalote. 365-378 [doi]
- Exploiting Traces in Program AnalysisAlex Groce, Rajeev Joshi. 379-393 [doi]
- Model-Checking Markov Chains in the Presence of UncertaintiesKoushik Sen, Mahesh Viswanathan, Gul Agha. 394-410 [doi]
- Safety Metric Temporal Logic Is Fully DecidableJoël Ouaknine, James Worrell. 411-425 [doi]
- Simulation-Based Graph SimilarityOleg Sokolsky, Sampath Kannan, Insup Lee. 426-440 [doi]
- PRISM: A Tool for Automatic Verification of Probabilistic SystemsAndrew Hinton, Marta Z. Kwiatkowska, Gethin J. Norman, David Parker. 441-444 [doi]
- DISTRIBUTOR and BCG_MERGE: Tools for Distributed Explicit State Space GenerationHubert Garavel, Radu Mateescu, Damien Bergamini, Adrian Curic, Nicolas Descoubes, Christophe Joubert, Irina Smarandache-Sturm, Gilles Stragier. 445-449 [doi]
- MCMAS: A Model Checker for Multi-agent SystemsAlessio Lomuscio, Franco Raimondi. 450-454 [doi]
- MSCan - A Tool for Analyzing MSC SpecificationsBenedikt Bollig, Carsten Kern, Markus Schlütter, Volker Stolz. 455-458 [doi]
- A Practical and Complete Approach to Predicate RefinementRanjit Jhala, Kenneth L. McMillan. 459-473 [doi]
- Counterexample Driven Refinement for Abstract InterpretationBhargav S. Gulavani, Sriram K. Rajamani. 474-488 [doi]
- Abstraction Refinement with Craig Interpolation and Symbolic Pushdown SystemsJavier Esparza, Stefan Kiefer, Stefan Schwoon. 489-503 [doi]