Abstract is missing.
- Singularity: Designing Better Software (Invited Talk)James R. Larus. 1-2 [doi]
- Coping with Outside-the-Box AttacksEdward W. Felten. 3-4 [doi]
- Assertion-Based Verification: Industry Myths to Realities (Invited Tutorial)Harry Foster. 5-10 [doi]
- Theorem Proving for Verification (Invited Tutorial)John Harrison. 11-18 [doi]
- Tutorial on Separation Logic (Invited Tutorial)Peter W. O Hearn. 19-21 [doi]
- Abstract Interpretation with Applications to Timing ValidationReinhard Wilhelm, Björn Wachter. 22-36 [doi]
- Reducing Concurrent Analysis Under a Context Bound to Sequential AnalysisAkash Lal, Thomas W. Reps. 37-51 [doi]
- Monitoring Atomicity in Concurrent ProgramsAzadeh Farzan, P. Madhusudan. 52-65 [doi]
- Dynamic Verification of MPI Programs with Reductions in Presence of Split Operations and Relaxed OrderingsSarvani S. Vakkalanka, Ganesh Gopalakrishnan, Robert M. Kirby. 66-79 [doi]
- A Hybrid Type System for Lock-Freedom of Mobile ProcessesNaoki Kobayashi, Davide Sangiorgi. 80-93 [doi]
- Implied Set Closure and Its Application to Memory Consistency VerificationSurender Baswana, Shashank K. Mehta, Vishal Powar. 94-106 [doi]
- Effective Program Verification for Relaxed Memory ModelsSebastian Burckhardt, Madanlal Musuvathi. 107-120 [doi]
- Mechanical Verification of Transactional Memories with Non-transactional Memory AccessesAriel Cohen 0002, Amir Pnueli, Lenore D. Zuck. 121-134 [doi]
- Automated Assume-Guarantee Reasoning by Abstraction RefinementMihaela Gheorghiu Bobaru, Corina S. Pasareanu, Dimitra Giannakopoulou. 135-148 [doi]
- Local Proofs for Linear-Time Properties of Concurrent ProgramsAriel Cohen 0002, Kedar S. Namjoshi. 149-161 [doi]
- Probabilistic CEGARHolger Hermanns, Björn Wachter, Lijun Zhang. 162-175 [doi]
- Computing Differential Invariants of Hybrid Systems as FixedpointsAndré Platzer, Edmund M. Clarke. 176-189 [doi]
- Constraint-Based Approach for Analysis of Hybrid SystemsSumit Gulwani, Ashish Tiwari. 190-203 [doi]
- AutoMOTGen: Automatic Model Oriented Test Generator for Embedded Control SystemsAmbar A. Gadkari, Anand Yeolekar, J. Suresh, S. Ramesh, Swarup Mohalik, K. C. Shashidhar. 204-208 [doi]
- FShell: Systematic Test Case Generation for Dynamic Analysis and MeasurementAndreas Holzer, Christian Schallhart, Michael Tautschnig, Helmut Veith. 209-213 [doi]
- Applying the Graph Minor Theorem to the Verification of Graph Transformation SystemsSalil Joshi, Barbara König. 214-226 [doi]
- Conflict-Tolerant FeaturesDeepak D Souza, Madhu Gopinathan. 227-239 [doi]
- Ranking Automata and Games for Prioritized RequirementsRajeev Alur, Aditya Kanade, Gera Weiss. 240-253 [doi]
- Efficient Craig Interpolation for Linear Diophantine (Dis)Equations and Linear Modular EquationsHimanshu Jain, Edmund M. Clarke, Orna Grumberg. 254-267 [doi]
- Linear Arithmetic with StarsRuzica Piskac, Viktor Kuncak. 268-280 [doi]
- Inferring Congruence Equations Using SATAndy King, Harald Søndergaard. 281-293 [doi]
- The Barcelogic SMT SolverMiquel Bofill, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell, Albert Rubio. 294-298 [doi]
- The MathSAT 4SMT SolverRoberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Roberto Sebastiani. 299-303 [doi]
- CSIsat: Interpolation for LA+EUFDirk Beyer, Damien Zufferey, Rupak Majumdar. 304-308 [doi]
- Prover s Palette: A User-Centric Approach to Verification with Isabelle and QEPCAD-BLaura I. Meikle, Jacques D. Fleuriot. 309-313 [doi]
- Heap Assumptions on DemandAndreas Podelski, Andrey Rybalchenko, Thomas Wies. 314-327 [doi]
- Proving Conditional TerminationByron Cook, Sumit Gulwani, Tal Lev-Ami, Andrey Rybalchenko, Mooly Sagiv. 328-340 [doi]
- Monotonic Abstraction for Programs with Dynamic Memory HeapsParosh Aziz Abdulla, Ahmed Bouajjani, Jonathan Cederberg, Frédéric Haziza, Ahmed Rezine. 341-354 [doi]
- Enhancing Program Verification with LemmasHuu Hai Nguyen, Wei-Ngan Chin. 355-369 [doi]
- A Numerical Abstract Domain Based on Expression Abstraction and Max Operator with Application in Timing AnalysisBhargav S. Gulavani, Sumit Gulwani. 370-384 [doi]
- Scalable Shape Analysis for Systems CodeHongseok Yang, Oukseh Lee, Josh Berdine, Cristiano Calcagno, Byron Cook, Dino Distefano, Peter W. O Hearn. 385-398 [doi]
- Thread Quantification for Concurrent Shape AnalysisJosh Berdine, Tal Lev-Ami, Roman Manevich, Ganesan Ramalingam, Shmuel Sagiv. 399-413 [doi]
- The Scyther Tool: Verification, Falsification, and Analysis of Security ProtocolsCas J. F. Cremers. 414-418 [doi]
- The CASPA Tool: Causality-Based Abstraction for Security Protocol AnalysisMichael Backes, Stefan Lorenz, Matteo Maffei, Kim Pecina. 419-422 [doi]
- Jakstab: A Static Analysis Platform for BinariesJohannes Kinder, Helmut Veith. 423-427 [doi]
- THOR: A Tool for Reasoning about Shape and ArithmeticStephen Magill, Ming-Hsien Tsai, Peter Lee, Yih-Kuen Tsay. 428-432 [doi]
- Functional Verification of Power Gated Designs by Compositional ReasoningCindy Eisner, Amir Nahir, Karen Yorav. 433-445 [doi]
- A Practical Approach to Word Level Model Checking of Industrial NetlistsPer Bjesse. 446-458 [doi]
- Validating High-Level SynthesisSudipta Kundu, Sorin Lerner, Rajesh Gupta. 459-472 [doi]
- An Algebraic Approach for Proving Data Correctness in Arithmetic Data PathsOliver Wienand, Markus Wedler, Dominik Stoffel, Wolfgang Kunz, Gert-Martin Greuel. 473-486 [doi]
- Application of Formal Word-Level Analysis to Constrained Random SimulationHyondeuk Kim, HoonSang Jin, Kavita Ravi, Petr Spacek, John Pierce, Robert P. Kurshan, Fabio Somenzi. 487-490 [doi]
- Producing Short Counterexamples Using Crucial Events Sujatha Kashyap, Vijay K. Garg. 491-503 [doi]
- Discriminative Model CheckingPeter Niebert, Doron Peled, Amir Pnueli. 504-516 [doi]
- Correcting a Space-Efficient Simulation AlgorithmRob J. van Glabbeek, Bas Ploeger. 517-529 [doi]
- Semi-external LTL Model CheckingStefan Edelkamp, Peter Sanders, Pavel Simecek. 530-542 [doi]
- QMC: A Model Checker for Quantum SystemsSimon J. Gay, Rajagopal Nagarajan, Nikolaos Papanikolaou. 543-547 [doi]
- T(O)RMC: A Tool for (omega)-Regular Model CheckingAxel Legay. 548-551 [doi]
- Faster Than Uppaal?Sebastian Kupferschmid, Martin Wehrle, Bernhard Nebel, Andreas Podelski. 552-555 [doi]