VeriFast: Imperative Programs as Proofs

No abstract is available for this paper.

• Publication year

  2010

• Venue

  Unknown venue

• Publication date

  2010-08-19

• Fields of study

  Computer Science

• Identifiers

  No identifiers available.

• External record

  Open on Semantic Scholar

• Source metadata

  Semantic Scholar

• No claims are published for this paper.

• No concepts are published for this paper.

• Mind the Gap A Verification Framework for Low-Level C

  2009cited by this paper
• VCC: Contract-based modular verification of concurrent C

  2009cited by this paper
• seL4: formal verification of an OS kernel

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

  2009cited by this paper
• Effective interactive proofs for higher-order imperative programs

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

  2008cited by this paper
• Verifying the Composite pattern using separation logic

  2008cited by this paper
• Scalable Shape Analysis for Systems Code

  2008cited by this paper
• Implicit dynamic frames

  2008cited by this paper
• Cyclic proofs of program termination in separation logic

  2008cited by this paper
• Separation Logic Contracts for a Java-Like Language with Fork/Join

  2008cited by this paper
• Full functional verification of linked data structures

  2008influential reference
• Z3: An Efficient SMT Solver

  2008cited by this paper
• ACSL: ANSI/ISO C Specification Language

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

  2008cited by this paper
• Modular Safety Checking for Fine-Grained Concurrency

  2007cited by this paper
• Local Reasoning for Storable Locks and Threads

  2007cited by this paper
• Proving that programs eventually do something good

  2007cited by this paper
• The Why/Krakatoa/Caduceus Platform for Deductive Program Verification

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

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

  2006cited by this paper
• Preliminary design of JML: a behavioral interface specification language for java

  2006cited by this paper
• Simplify: a theorem prover for program checking

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

  2005influential reference
• Separation logic and abstraction

  2005cited by this paper
• Interactive Theorem Proving and Program Development

  2004cited by this paper
• The Spec# Programming System: An Overview

  2004cited by this paper
• Extended static checking for Java

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

  2002cited by this paper
• Larch: Languages and Tools for Formal Specification

  1993cited by this paper

• A Hoare Logic with Regular Behavioral Specifications

  2022cites this paper
• Automated Verification of Parallel Nested DFS

  2020cites this paper
• Prescriptive Safety-Checks through Automated Proofs for Control-Flow Integrity

  2016cites this paper
• Concurrent separation logic

  2016cites this paper
• Theorem Prover Based Static Analyzer: Comparison Analysis Between ESC/Java2 and KeY

  2015cites this paper
• AutoProof: auto-active functional verification of object-oriented programs

  2015cites this paper
• Rotation of Sequences: Algorithms and Proofs

  2014cites this paper
• A proof system for separation logic with magic wand

  2014influential citation
• Co-induction Simply - Automatic Co-inductive Proofs in a Program Verifier

  2014cites this paper
• Witnessing the elimination of magic wands

  2013influential citation
• Co-induction in an Auto-Active Program

  2013cites this paper
• Automating Theorem Proving with SMT

  2013cites this paper
• A theorem prover for Boolean BI

  2013cites this paper
• Verified Calculations

  2013cites this paper
• Automating Induction with an SMT Solver

  2012cites this paper
• Computational Logic and Quantier Elimination Techniques for (Semi-)automatic Static Analysis and Synthesis of Algorithms

  2012cites this paper
• International Workshop on Automated Verification of Critical Systems ( AVoCS 2012 ) Semi-automatic Proofs about Object Graphs in Separation Logic

  2012cites this paper
• Comparing Verification Condition Generation with Symbolic Execution: An Experience Report

  2012influential citation
• Developing verified programs with Dafny

  2012cites this paper
• A Programmer-Centric Approach to Program Verification in ATS

  2012cites this paper
• Software Verification with Towers of Abstractions

  2011cites this paper
• Enforcing Structural Invariants Using Dynamic Frames

  2011cites this paper
• Working Towards the Verified Software Process

  2010influential citation