Abstract is missing.
- Abstract Domains for Automated Reasoning about List-Manipulating Programs with Infinite DataAhmed Bouajjani, Cezara Dragoi, Constantin Enea, Mihaela Sighireanu. 1-22 [doi]
- Software Verification with Liquid TypesRanjit Jhala. 23 [doi]
- Teaching Semantics with a Proof Assistant: No More LSD Trip ProofsTobias Nipkow. 24-38 [doi]
- Whale: An Interpolation-Based Algorithm for Inter-procedural VerificationAws Albarghouthi, Arie Gurfinkel, Marsha Chechik. 39-55 [doi]
- Synchronizability for Verification of Asynchronously Communicating SystemsSamik Basu, Tevfik Bultan, Meriem Ouederni. 56-71 [doi]
- On the Termination of Integer LoopsAmir M. Ben-Amram, Samir Genaim, Abu Naser Masud. 72-87 [doi]
- Verification of Gap-Order Constraint Abstractions of Counter SystemsLaura Bozzelli, Sophie Pinchinat. 88-103 [doi]
- On Application of Multi-Rooted Binary Decision Diagrams to Probabilistic Model CheckingDmitry Bugaychenko. 104-118 [doi]
- Regression Verification for Multi-threaded ProgramsSagar Chaki, Arie Gurfinkel, Ofer Strichman. 119-135 [doi]
- Crowfoot: A Verifier for Higher-Order Store ProgramsNathaniel Charlton, Ben Horsfall, Bernhard Reus. 136-151 [doi]
- Synthesizing Protocols for Digital Contract SigningKrishnendu Chatterjee, Vishwanath Raman. 152-168 [doi]
- Model Checking Information Flow in Reactive SystemsRayna Dimitrova, Bernd Finkbeiner, Máté Kovács, Markus N. Rabe, Helmut Seidl. 169-185 [doi]
- Splitting via InterpolantsEvren Ermis, Jochen Hoenicke, Andreas Podelski. 186-201 [doi]
- Automatic Inference of Access PermissionsPietro Ferrara, Peter Müller. 202-218 [doi]
- Lazy SynthesisBernd Finkbeiner, Swen Jacobs. 219-234 [doi]
- Donut Domains: Efficient Non-convex Domains for Abstract InterpretationKhalil Ghorbal, Franjo Ivancic, Gogul Balakrishnan, Naoto Maeda, Aarti Gupta. 235-250 [doi]
- Inferring Canonical Register AutomataFalk Howar, Bernhard Steffen, Bengt Jonsson, Sofia Cassel. 251-266 [doi]
- Alternating Control Flow ReconstructionJohannes Kinder, Dmitry Kravchenko. 267-282 [doi]
- Effective Synthesis of Asynchronous Systems from GR(1) SpecificationsUri Klein, Nir Piterman, Amir Pnueli. 283-298 [doi]
- Sound Non-statistical Clustering of Static Analysis AlarmsWoosuk Lee, Wonchan Lee, Kwangkeun Yi. 299-314 [doi]
- Automating Induction with an SMT SolverK. Rustan M. Leino. 315-331 [doi]
- Modeling Asynchronous Message Passing for C ProgramsEverett Morse, Nick Vrvilo, Eric Mercer, Jay McCarthy. 332-347 [doi]
- Local Symmetry and Compositional VerificationKedar S. Namjoshi, Richard J. Trefler. 348-362 [doi]
- versat: A Verified Modern SAT SolverDuckki Oe, Aaron Stump, Corey Oliver, Kevin Clancy. 363-378 [doi]
- Decision Procedures for Region LogicStan Rosenberg, Anindya Banerjee, David A. Naumann. 379-395 [doi]
- A General Framework for Probabilistic Characterizing FormulaeJoshua Sack, Lijun Zhang 0001. 396-411 [doi]
- Loop Invariant Symbolic Execution for Parallel ProgramsStephen F. Siegel, Timothy K. Zirkel. 412-427 [doi]
- Synthesizing Efficient ControllersChristian von Essen, Barbara Jobstmann. 428-444 [doi]
- Ideal Abstractions for Well-Structured Transition SystemsDamien Zufferey, Thomas Wies, Thomas A. Henzinger. 445-460 [doi]