VeriFast
From MaRDI portal
Software:19722
No author found.
Related Items (68)
Formal verification of parallel prefix sum and stream compaction algorithms in CUDA ⋮ Verifying Array Manipulating Programs with Full-Program Induction ⋮ Automated Verification of Parallel Nested DFS ⋮ Concise Read-Only Specifications for Better Synthesis of Programs with Pointers ⋮ Local Reasoning for Global Graph Properties ⋮ Crowfoot: A Verifier for Higher-Order Store Programs ⋮ Automatic Inference of Access Permissions ⋮ Automating Induction with an SMT Solver ⋮ Symbolic execution proofs for higher order store programs ⋮ 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 ⋮ Caper ⋮ Disproving Inductive Entailments in Separation Logic via Base Pair Approximation ⋮ Abstraction and subsumption in modular verification of C programs ⋮ Two for the Price of One: Lifting Separation Logic Assertions ⋮ Generalized arrays for Stainless frames ⋮ Instrumenting a weakest precondition calculus for counterexample generation ⋮ Shape Neutral Analysis of Graph-based Data-structures ⋮ Featherweight VeriFast ⋮ Model Checking MSVL Programs Based on Dynamic Symbolic Execution ⋮ Traits: correctness-by-construction for free ⋮ A theorem prover for Boolean BI ⋮ Verifying data- and control-oriented properties combining static and runtime verification: theory and tools ⋮ Compositional Invariant Checking for Overlaid and Nested Linked Lists ⋮ Automating Theorem Proving with SMT ⋮ A Program Construction and Verification Tool for Separation Logic ⋮ Specification patterns for reasoning about recursion through the store ⋮ Stepwise refinement of heap-manipulating code in Chalice ⋮ Using formal reasoning on a model of tasks for FreeRTOS ⋮ Unified Reasoning About Robustness Properties of Symbolic-Heap Separation Logic ⋮ Predicate extension of symbolic memory graphs for the analysis of memory safety correctness ⋮ Deductive verification of floating-point Java programs in KeY ⋮ A generic framework for symbolic execution: a coinductive approach ⋮ Expressive modular fine-grained concurrency specification ⋮ RGITL: a temporal logic framework for compositional reasoning about interleaved programs ⋮ Verification of Concurrent Systems with VerCors ⋮ One Logic to Use Them All ⋮ Automatic verification of Java programs with dynamic frames ⋮ A Shape Analysis for Non-linear Data Structures ⋮ Viper: A Verification Infrastructure for Permission-Based Reasoning ⋮ Backwards and forwards with separation logic ⋮ Dafny: An Automatic Program Verifier for Functional Correctness ⋮ Interleaving Symbolic Execution and Partial Evaluation ⋮ Static Contract Checking with Abstract Interpretation ⋮ Exploiting pointer analysis in memory models for deductive verification ⋮ Sound, Modular and Compositional Verification of the Input/Output Behavior of Programs ⋮ A Basis for Verifying Multi-threaded Programs ⋮ Unifying separation logic and region logic to allow interoperability ⋮ Simpler proofs with decentralized invariants ⋮ Specification Patterns and Proofs for Recursion through the Store ⋮ Tractable Reasoning in a Fragment of Separation Logic ⋮ A relational shape abstract domain ⋮ Automatic Parallelization and Optimization of Programs by Proof Rewriting ⋮ A Machine-Checked Framework for Relational Separation Logic ⋮ Model checking for symbolic-heap separation logic with inductive predicates ⋮ Charge! ⋮ Considerate Reasoning and the Composite Design Pattern ⋮ Efficient verification of imperative programs using auto2 ⋮ Automating deductive verification for weak-memory programs ⋮ Invariants Synthesis over a Combined Domain for Automated Program Verification ⋮ Proving Correctness and Security of Two-Party Computation Implemented in Java in Presence of a Semi-honest Sender ⋮ Practical abstractions for automated verification of shared-memory concurrency ⋮ A verification-driven framework for iterative design of controllers ⋮ Verifying Whiley programs with Boogie ⋮ On Symbolic Heaps Modulo Permission Theories ⋮ Behavioral interface specification languages ⋮ A Decision Procedure for Guarded Separation Logic Complete Entailment Checking for Separation Logic with Inductive Definitions
This page was built for software: VeriFast
