Abstract is missing.
- Cyber War, Formal Verification and Certified InfrastructureWolfgang Paul. 1 [doi]
- A Certified Multi-prover Verification Condition GeneratorPaolo Herms, Claude Marché, Benjamin Monate. 2-17 [doi]
- Integrated Semantics of Intermediate-Language C and Macro-Assembler for Pervasive Formal Verification of Operating Systems and Hypervisors from VerisoftXTSabine Schmaltz, Andrey Shadrin. 18-33 [doi]
- The Location Linking Concept: A Basis for Verification of Code Using PointersGregory Kulczycki, Hampton Smith, Heather K. Harton, Murali Sitaraman, William F. Ogden, Joseph E. Hollingsworth. 34-49 [doi]
- Verifying Implementations of Security Protocols by RefinementNadia Polikarpova, Michal Moskal. 50-65 [doi]
- Deciding Functional Lists with Sublist SetsThomas Wies, Marco Muñiz, Viktor Kuncak. 66-81 [doi]
- Developing Verified Programs with DafnyK. Rustan M. Leino. 82 [doi]
- Verifying Two Lines of C with Why3: An Exercise in Program VerificationJean-Christophe Filliâtre. 83-97 [doi]
- Development and Evaluation of LAV: An SMT-Based Error Finding Platform - System DescriptionMilena Vujosevic-Janicic, Viktor Kuncak. 98-113 [doi]
- A Lightweight Technique for Distributed and Incremental Program VerificationMartin Brain, Florian Schanda. 114-129 [doi]
- A Comparison of Intermediate Verification Languages: Boogie and Sireum/PilarLoren Segal, Patrice Chalin. 130-145 [doi]
- LLBMC: Bounded Model Checking of C and C++ Programs Using a Compiler IRFlorian Merz, Stephan Falke, Carsten Sinz. 146-161 [doi]
- The Marriage of Exploration and DeductionRupak Majumdar. 162 [doi]
- Modeling and Validating the Train Fare Calculation and Adjustment System Using VDM++Nguyen Van Tang, Daisuke Souma, Goro Hatayama, Hitoshi Ohsaki. 163-178 [doi]
- Formalized Verification of Snapshotable Trees: Separation and SharingHannes Mehnert, Filip Sieczkowski, Lars Birkedal, Peter Sestoft. 179-195 [doi]
- Comparing Verification Condition Generation with Symbolic Execution: An Experience ReportIoannis T. Kassios, Peter Müller, Malte Schwerhoff. 196-208 [doi]
- Verification of TLB Virtualization Implemented in CEyad Alkassar, Ernie Cohen, Mikhail Kovalev, Wolfgang J. Paul. 209-224 [doi]
- Formalization and Analysis of Real-Time Requirements: A Feasibility Study at BOSCHAmalinda Post, Jochen Hoenicke. 225-240 [doi]
- Our Experience with the CodeContracts Static Checker - (Invited Tutorial)Francesco Logozzo. 241-242 [doi]
- Isabelle/Circus: A Process Specification and Verification EnvironmentAbderrahmane Feliachi, Marie-Claude Gaudel, Burkhart Wolff. 243-260 [doi]
- Termination Analysis of Imperative Programs Using Bitvector ArithmeticStephan Falke, Deepak Kapur, Carsten Sinz. 261-277 [doi]
- Specifying and Verifying the Correctness of Dynamic Software UpdatesChristopher M. Hayden, Stephen Magill, Michael Hicks, Nate Foster, Jeffrey S. Foster. 278-293 [doi]
- Symbolic Execution Enhanced System TestingMisty Davies, Corina S. Pasareanu, Vishwanath Raman. 294-309 [doi]
- Infeasible Code DetectionCristiano Bertolini, Martin Schäf, Pascal Schweitzer. 310-325 [doi]