Abstract is missing.
- Proving Program Invariance and Termination by Parametric Abstraction, Lagrangian Relaxation and Semidefinite ProgrammingPatrick Cousot. 1-24 [doi]
- Scalable Analysis of Linear Systems Using Mathematical ProgrammingSriram Sankaranarayanan, Henny B. Sipma, Zohar Manna. 25-41 [doi]
- The Arithmetic-Geometric Progression Abstract DomainJérôme Feret. 42-58 [doi]
- An Overview of Semantics for the Validation of Numerical ProgramsMatthieu Martel. 59-77 [doi]
- The Verifying Compiler, a Grand Challenge for Computing ResearchC. A. R. Hoare. 78-78 [doi]
- Checking Herbrand Equalities and BeyondMarkus Müller-Olm, Oliver Rüthing, Helmut Seidl. 79-96 [doi]
- Static Analysis by Abstract Interpretation of the Quasi-synchronous Composition of Synchronous ProgramsJulien Bertrane. 97-112 [doi]
- Termination of Polynomial ProgramsAaron R. Bradley, Zohar Manna, Henny B. Sipma. 113-129 [doi]
- Verifying Safety of a Token Coherence Implementation by Parametric Compositional RefinementSebastian Burckhardt, Rajeev Alur, Milo M. K. Martin. 130-145 [doi]
- Abstraction for LivenessAmir Pnueli. 146-146 [doi]
- Abstract Interpretation with Alien Expressions and Heap StructuresBor-Yuh Evan Chang, K. Rustan M. Leino. 147-163 [doi]
- Shape Analysis by Predicate AbstractionIttai Balaban, Amir Pnueli, Lenore D. Zuck. 164-180 [doi]
- Predicate Abstraction and Canonical Abstraction for Singly-Linked ListsRoman Manevich, Eran Yahav, Ganesan Ramalingam, Shmuel Sagiv. 181-198 [doi]
- Purity and Side Effect Analysis for Java ProgramsAlexandru Salcianu, Martin C. Rinard. 199-215 [doi]
- Automata as AbstractionsDennis Dams, Kedar S. Namjoshi. 216-232 [doi]
- ::::Don t Know:::: in the µ-CalculusOrna Grumberg, Martin Lange, Martin Leucker, Sharon Shoham. 233-249 [doi]
- Model Checking of Systems Employing Commutative FunctionsA. Prasad Sistla, Min Zhou, Xiaodong Wang. 250-266 [doi]
- Weak Automata for the Linear Time µ-CalculusMartin Lange. 267-281 [doi]
- Model Checking for Process Rewrite Systems and a Class of Action-Based Regular PropertiesLaura Bozzelli. 282-297 [doi]
- Minimizing Counterexample with Unit Core Extraction and Incremental SATShengYu Shen, Ying Qin, Sikun Li. 298-312 [doi]
- I/O Efficient Directed Model CheckingShahid Jabbar, Stefan Edelkamp. 313-329 [doi]
- Verification of an Error Correcting Code by Abstract InterpretationCharles Hymans. 330-345 [doi]
- Information Flow Analysis for Java BytecodeSamir Genaim, Fausto Spoto. 346-362 [doi]
- Cryptographic Protocol Analysis on Real C CodeJean Goubault-Larrecq, Fabrice Parrennes. 363-379 [doi]
- Simple Is Better: Efficient Bounded Model Checking for Past LTLTimo Latvala, Armin Biere, Keijo Heljanko, Tommi A. Junttila. 380-395 [doi]
- Optimizing Bounded Model Checking for Linear Hybrid SystemsErika Ábrahám, Bernd Becker, Felix Klaedtke, Martin Steffen. 396-412 [doi]
- Efficient Verification of Halting Properties for MPI Programs with Wildcard ReceivesStephen F. Siegel. 413-429 [doi]
- Generalized Typestate Checking for Data Structure ConsistencyPatrick Lam, Viktor Kuncak, Martin C. Rinard. 430-447 [doi]
- On the Complexity of Error ExplanationNirman Kumar, Viraj Kumar, Mahesh Viswanathan. 448-464 [doi]
- Efficiently Verifiable Conditions for Deadlock-Freedom of Large Concurrent ProgramsPaul C. Attie, Hana Chockler. 465-481 [doi]