Comparing Verification Condition Generation with Symbolic Execution: An Experience Report

No abstract is available for this paper.

• Publication year

  2012

• Venue

  Verified Software: Theories, Tools, Experiments

• Publication date

  2012-01-28

• Fields of study

  Computer Science

• Identifiers
  DOI 10.1007/978-3-642-27705-4_16
• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Foundations of Security Analysis and Design VII

  2014cited by this paper
• L T A

  2011cited by this paper
• The Relationship between Separation Logic and Implicit Dynamic Frames

  2011cited by this paper
• The 1st Verified Software Competition: Experience Report

  2011cited by this paper
• Formal Verification of Object-Oriented Software - International Conference, FoVeOOS 2010, Paris, France, June 28-30, 2010, Revised Selected Papers

  2011cited by this paper
• Rigorous Software Development - An Introduction to Program Verification

  2011cited by this paper
• Using Debuggers to Understand Failed Verification Attempts

  2011cited by this paper
• FM 2011: Formal Methods - 17th International Symposium on Formal Methods, Limerick, Ireland, June 20-24, 2011. Proceedings

  2011cited by this paper
• Fractional permissions without the fractions

  2011cited by this paper
• Verifying C Programs

  2011cited by this paper
• Symbolic execution for chalice

  2011cited by this paper
• Dynamic Frames in Java Dynamic Logic

  2010cited by this paper
• VeriFast: Imperative Programs as Proofs

  2010influential reference
• Formal Methods for Components and Objects - 8th International Symposium, FMCO 2009, Eindhoven, The Netherlands, November 4-6, 2009. Revised Selected Papers

  2010cited by this paper
• Amortised Memory Analysis Using the Depth of Data Structures

  2009cited by this paper
• Verification of Concurrent Programs with Chalice

  2009cited by this paper
• Implicit Dynamic Frames: Combining Dynamic Frames and Separation Logic

  2009influential reference
• A Basis for Verifying Multi-threaded Programs

  2009cited by this paper
• ECOOP 2009 - Object-Oriented Programming, 23rd European Conference, Genoa, Italy, July 6-10, 2009. Proceedings

  2009cited by this paper
• VCC: A Practical System for Verifying Concurrent C

  2009cited by this paper
• ECOOP 2008 - Object-Oriented Programming, 22nd European Conference, Paphos, Cyprus, July 7-11, 2008, Proceedings

  2008cited by this paper
• jStar: towards practical verification for java

  2008cited by this paper
• Regional Logic for Local Reasoning about Global Invariants

  2008cited by this paper
• Z3: An Efficient SMT Solver

  2008cited by this paper
• Formalising Java's Data Race Free Guarantee

  2007cited by this paper
• Verification of Object-Oriented Software. The KeY Approach - Foreword by K. Rustan M. Leino

  2007cited by this paper
• Compositional Class Refinement in Object-Z

  2006cited by this paper
• Dynamic Frames: Support for Framing, Dependencies and Sharing Without Restrictions

  2006cited by this paper
• Beyond Assertions: Advanced Specification and Verification with JML and ESC/Java2

  2005cited by this paper
• Smallfoot: Modular Automatic Assertion Checking with Separation Logic

  2005cited by this paper
• Object Invariants in Dynamic Contexts

  2004cited by this paper
• A Temporal Logic of Nested Calls and Returns

  2004cited by this paper
• ECOOP 2004 – Object-Oriented Programming

  2004cited by this paper
• Checking Interference with Fractional Permissions

  2003cited by this paper
• Separation logic: a logic for shared mutable data structures

  2002cited by this paper
• JML: A Notation for Detailed Design

  1999cited by this paper
• A Discipline of Programming

  1976cited by this paper
• Symbolic execution and program testing

  1976cited by this paper

• Raven: An SMT-Based Concurrency Verifier

  2025cites this paper
• Verification Algorithms for Automated Separation Logic Verifiers

  2024cites this paper
• Layered Formal Verification of a TCP Stack

  2021cites this paper
• Improving Performance of the VerCors Program Verifier

  2020cites this paper
• Deductive Software Verification: Future Perspectives: Reflections on the Occasion of 20 Years of KeY

  2020cites this paper
• Deductive Software Verification: From Pen-and-Paper Proofs to Industrial Tools

  2019cites this paper
• Using Isabelle/UTP for the Verification of Sorting Algorithms: A Case Study

  2019cites this paper
• p4v: practical verification for programmable data planes

  2018cites this paper
• Integrating deductive verification and symbolic execution for abstract object creation in dynamic logic

  2016cites this paper
• Viper A Verification Infrastructure for Permission-Based Reasoning

  2014cites this paper
• Matching Spec# Specifications

  2013cites this paper
• Verification Condition Generation for Permission Logics with Abstract Predicates and Abstraction Functions

  2013cites this paper
• Implementation-level verification of algorithms with KeY

  2013cites this paper
• Witnessing the elimination of magic wands

  2013cites this paper
• An Empirical Study of Path Feasibility Queries

  2013cites this paper
• Abstract Read Permissions: Fractional Permissions without the Fractions

  2013cites this paper
• Verification Condition Generation for Permission Logics with Abstraction Functions

  2012cites this paper
• Supporting subclassing and traits in Syxc

  2012cites this paper
• Soundness of a Logic-Based Verification Method for Imperative Loops

  2012cites this paper
• Fractional permissions without the fractions

  2011cites this paper
• Using Isabelle/UTP for the Verification of Sorting Algorithms A Case Study

  year unknowninfluential citation