VeriFast

swMATH7705MaRDI QIDQ19722FDOQ19722

Author name not available (Why is that?)

Official website: http://people.cs.kuleuven.be/~bart.jacobs/verifast/

Cited In (85)

• Automating theorem proving with SMT
• Sound, modular and compositional verification of the input/output behavior of programs
• Shape neutral analysis of graph-based data-structures
• Two for the price of one: lifting separation logic assertions
• On Symbolic Heaps Modulo Permission Theories
• MoSeL
• Proving Correctness and Security of Two-Party Computation Implemented in Java in Presence of a Semi-honest Sender
• Verifying data- and control-oriented properties combining static and runtime verification: theory and tools
• Automatic Parallelization and Optimization of Programs by Proof Rewriting
• Interleaving symbolic execution and partial evaluation
• Automatic inference of access permissions
• Featherweight VeriFast
• Model Checking MSVL Programs Based on Dynamic Symbolic Execution
• Verifying array manipulating programs with full-program induction
• Specification patterns for reasoning about recursion through the store
• RGITL: a temporal logic framework for compositional reasoning about interleaved programs
• A theorem prover for Boolean BI
• Verifying Whiley programs with Boogie
• SableJBDD
• Formal verification of a Java component using the RESOLVE framework
• Deductive synthesis of programs with pointers: techniques, challenges, opportunities (invited paper)
• Ghost signals: verifying termination of busy waiting
• Efficient verification of imperative programs using auto2
• Considerate reasoning and the Composite design pattern
• Model checking for symbolic-heap separation logic with inductive predicates
• Disproving inductive entailments in separation logic via base pair approximation
• Automating Induction with an SMT Solver
• BDD
• JDD
• Automatic verification of Java programs with dynamic frames
• Formal verification of parallel prefix sum and stream compaction algorithms in CUDA
• Deductive verification of floating-point Java programs in KeY
• Symbolic execution proofs for higher order store programs
• A Shape Analysis for Non-linear Data Structures
• A Basis for Verifying Multi-threaded Programs
• Viper: a verification infrastructure for permission-based reasoning
• Concise read-only specifications for better synthesis of programs with pointers
• Local reasoning for global graph properties
• Automated verification of parallel nested DFS
• Simpler proofs with decentralized invariants
• A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
• Automating deductive verification for weak-memory programs
• Instrumenting a weakest precondition calculus for counterexample generation
• Behavioral interface specification languages
• Generalized arrays for Stainless frames
• Predicate extension of symbolic memory graphs for the analysis of memory safety correctness
• Static contract checking with abstract interpretation
• ACSL
• Caduceus
• Frama-C
• Why3
• Spec#
• Charge! A framework for higher-order separation logic in Coq
• HighSpec
• SLAyer
• FixBag
• WhyML
• VeriCool
• FunArray
• Backwards and forwards with separation logic
• Specification patterns and proofs for recursion through the store
• OpenJML
• Traits: correctness-by-construction for free
• Using formal reasoning on a model of tasks for FreeRTOS
• Unifying separation logic and region logic to allow interoperability
• A program construction and verification tool for separation logic
• Stepwise refinement of heap-manipulating code in Chalice
• Exploiting pointer analysis in memory models for deductive verification
• A relational shape abstract domain
• A generic framework for symbolic execution: a coinductive approach
• Practical abstractions for automated verification of shared-memory concurrency
• One logic to use them all
• Oclgrind
• Tractable Reasoning in a Fragment of Separation Logic
• Abstraction and subsumption in modular verification of C programs
• Compositional invariant checking for overlaid and nested linked lists
• A verification-driven framework for iterative design of controllers
• A machine-checked framework for relational separation logic
• Crowfoot: A Verifier for Higher-Order Store Programs
• Dafny: an automatic program verifier for functional correctness
• Invariants synthesis over a combined domain for automated program verification
• Verification of concurrent systems with VerCors
• Caper
• Expressive modular fine-grained concurrency specification
• Unified reasoning about robustness properties of symbolic-heap separation logic

This page was built for software: VeriFast