Abstract is missing.
- From Retrospective Verification to Forward-Looking DevelopmentK. Rustan M. Leino. 1 [doi]
- Specifications for FreeAndreas Zeller. 2-12 [doi]
- The Theory and Practice of SALTAndreas Bauer 0002, Martin Leucker. 13-40 [doi]
- VeriFast: A Powerful, Sound, Predictable, Fast Verifier for C and JavaBart Jacobs, Jan Smans, Pieter Philippaerts, Frédéric Vogels, Willem Penninckx, Frank Piessens. 41-55 [doi]
- Verifying Functional Correctness of C Programs with VCCMichal Moskal. 56-57 [doi]
- Bakar Kiasan: Flexible Contract Checking for Critical Systems Using Symbolic ExecutionJason Belt, John Hatcliff, Robby, Patrice Chalin, David Hardin, Xianghua Deng. 58-72 [doi]
- Approximate Quantifier Elimination for Propositional Boolean FormulaeJörg Brauer, Andy King. 73-88 [doi]
- Towards Flight Control Verification Using Automated Theorem ProvingWilliam Denman, Mohamed H. Zaki, Sofiène Tahar, Luis Rodrigues. 89-100 [doi]
- Generalized Rabin(1) Synthesis with Applications to Robust System SynthesisRüdiger Ehlers. 101-115 [doi]
- Integrating an Automated Theorem Prover into AgdaSimon Foster, Georg Struth. 116-130 [doi]
- Efficient Predicate Abstraction of Program SummariesArie Gurfinkel, Sagar Chaki, Samir Sapra. 131-145 [doi]
- Synthesis for PCTL in Parametric Markov Decision ProcessesErnst Moritz Hahn, Tingting Han, Lijun Zhang. 146-161 [doi]
- Formalizing Probabilistic Safety ClaimsHeber Herencia-Zapana, George Hagen, Anthony Narkawicz. 162-176 [doi]
- The OpenTheory Standard Theory LibraryJoe Hurd. 177-191 [doi]
- Instantiation-Based Invariant DiscoveryTemesghen Kahsai, Yeting Ge, Cesare Tinelli. 192-206 [doi]
- Stuttering Mostly Speeds Up Solving Parity GamesSjoerd Cranen, Jeroen J. A. Keiren, Tim A. C. Willemse. 207-221 [doi]
- Counterexample-Based Error Localization of Behavior ModelsTsutomu Kumazawa, Tetsuo Tamai. 222-236 [doi]
- Call InvariantsShuvendu K. Lahiri, Shaz Qadeer. 237-251 [doi]
- Symmetry for the Analysis of Dynamic SystemsZarrin Langari, Richard J. Trefler. 252-266 [doi]
- Implementing Cryptographic Primitives in the Symbolic ModelPeeter Laud. 267-281 [doi]
- Model Checking Using SMT and Theory of ListsAleksandar Milicevic, Hillel Kugler. 282-297 [doi]
- Automated Test Case Generation with SMT-Solving and Abstract InterpretationJan Peleska, Elena Vorobev, Florian Lapschies. 298-312 [doi]
- Generating Data Race Witnesses by an SMT-Based AnalysisMahmoud Said, Chao Wang, Zijiang Yang, Karem A. Sakallah. 313-327 [doi]
- Applying Atomicity and Model Decomposition to a Space Craft System in Event-BAsieh Salehi Fathabadi, Abdolbaghi Rezazadeh, Michael Butler. 328-342 [doi]
- A Theory of Skiplists with Applications to the Verification of Concurrent DatatypesAlejandro Sánchez, César Sánchez. 343-358 [doi]
- CORAL: Solving Complex Constraints for Symbolic PathFinderMatheus Souza, Mateus Borges, Marcelo d Amorim, Corina S. Pasareanu. 359-374 [doi]
- Automated Formal Verification of the ::::TTEthernet:::: Synchronization QualityWilfried Steiner, Bruno Dutertre. 375-390 [doi]
- Extending the GWV Security Policy and Its Modular Application to a Separation KernelSergey Tverdyshev. 391-405 [doi]
- Combining Partial-Order Reduction and Symbolic Model Checking to Verify LTL PropertiesJosé Vander Meulen, Charles Pecheur. 406-421 [doi]
- Towards Informed Swarm VerificationAnton Wijs. 422-437 [doi]
- Scaling Up with Event-B: A Case StudyFaqing Yang, Jean-Pierre Jacquot. 438-452 [doi]
- D-Finder 2: Towards Efficient Correctness of Incremental DesignSaddek Bensalem, Andreas Griesmayer, Axel Legay, Thanh-Hung Nguyen, Joseph Sifakis, Rongjie Yan. 453-458 [doi]
- Infer: An Automatic Program Verifier for Memory Safety of C ProgramsCristiano Calcagno, Dino Distefano. 459-465 [doi]
- Model Construction and Priority Synthesis for Simple Interaction SystemsChih-Hong Cheng, Saddek Bensalem, Barbara Jobstmann, Rongjie Yan, Alois Knoll, Harald Ruess. 466-471 [doi]
- OpenJML: JML for Java 7 by Extending OpenJDKDavid R. Cok. 472-479 [doi]
- jSMTLIB: Tutorial, Validation and Adapter Tools for SMT-LIBv2David R. Cok. 480-486 [doi]
- opaal: A Lattice Model CheckerAndreas Engelbredt Dalsgaard, René Rydhof Hansen, Kenneth Yrke Jørgensen, Kim Guldstrand Larsen, Mads Chr. Olesen, Petur Olsen, Jirí Srba. 487-493 [doi]
- A Tabular Expression Toolbox for Matlab/SimulinkColin Eles, Mark Lawford. 494-499 [doi]
- ::::LLVM2CSP::::: Extracting CSP Models from Concurrent ProgramsMoritz Kleine, Björn Bartels, Thomas Göthel, Steffen Helke, Dirk Prenzel. 500-505 [doi]
- Multi-Core LTSmin: Marrying Modularity and ScalabilityAlfons Laarman, Jaco van de Pol, Michael Weber 0002. 506-511 [doi]
- GiNaCRA: A C++ Library for Real Algebraic ComputationsUlrich Loup, Erika Ábrahám. 512-517 [doi]
- Kopitiam: Modular Incremental Interactive Full Functional Static Verification of Java CodeHannes Mehnert. 518-524 [doi]
- Milestones: A Model Checker Combining Symbolic Model Checking and Partial Order ReductionJosé Vander Meulen, Charles Pecheur. 525-531 [doi]