VeriFast

swMATH7705MaRDI QIDQ19722FDOQ19722

Author name not available (Why is that?)

Cited In (68)

• Interleaving Symbolic Execution and Partial Evaluation
• On Symbolic Heaps Modulo Permission Theories
• Proving Correctness and Security of Two-Party Computation Implemented in Java in Presence of a Semi-honest Sender
• Shape Neutral Analysis of Graph-based Data-structures
• Automatic Parallelization and Optimization of Programs by Proof Rewriting
• Featherweight VeriFast
• Model Checking MSVL Programs Based on Dynamic Symbolic Execution
• 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
• 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
• Automatic Inference of Access Permissions
• Model checking for symbolic-heap separation logic with inductive predicates
• Automating Induction with an SMT Solver
• Invariants Synthesis over a Combined Domain for Automated Program Verification
• A Machine-Checked Framework for Relational Separation Logic
• Dafny: An Automatic Program Verifier for Functional Correctness
• Charge!
• Automatic verification of Java programs with dynamic frames
• Two for the price of one: lifting separation logic assertions
• Formal verification of parallel prefix sum and stream compaction algorithms in CUDA
• Deductive verification of floating-point Java programs in KeY
• Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic
• Symbolic execution proofs for higher order store programs
• A Shape Analysis for Non-linear Data Structures
• A Basis for Verifying Multi-threaded Programs
• Simpler proofs with decentralized invariants
• A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
• One Logic to Use Them All
• Automating deductive verification for weak-memory programs
• Instrumenting a weakest precondition calculus for counterexample generation
• Sound, Modular and Compositional Verification of the Input/Output Behavior of Programs
• Behavioral interface specification languages
• Compositional Invariant Checking for Overlaid and Nested Linked Lists
• Disproving Inductive Entailments in Separation Logic via Base Pair Approximation
• Generalized arrays for Stainless frames
• Considerate Reasoning and the Composite Design Pattern
• Viper: A Verification Infrastructure for Permission-Based Reasoning
• Predicate extension of symbolic memory graphs for the analysis of memory safety correctness
• Verification of Concurrent Systems with VerCors
• Backwards and forwards with separation logic
• Verifying Array Manipulating Programs with Full-Program Induction
• 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
• 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
• Verifying data- and control-oriented properties combining static and runtime verification: theory and tools
• Practical abstractions for automated verification of shared-memory concurrency
• Tractable Reasoning in a Fragment of Separation Logic
• Abstraction and subsumption in modular verification of C programs
• A verification-driven framework for iterative design of controllers
• Static Contract Checking with Abstract Interpretation
• Crowfoot: A Verifier for Higher-Order Store Programs
• Specification Patterns and Proofs for Recursion through the Store
• Automating Theorem Proving with SMT
• Concise Read-Only Specifications for Better Synthesis of Programs with Pointers
• Local Reasoning for Global Graph Properties
• Automated Verification of Parallel Nested DFS
• A Program Construction and Verification Tool for Separation Logic
• Caper
• Expressive modular fine-grained concurrency specification

This page was built for software: VeriFast