Software:19722: Difference between revisions
From MaRDI portal
Software:19722
Created automatically from import240305080343 |
(No difference)
|
Latest revision as of 20:10, 5 March 2024
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
