swMATH7714MaRDI QIDQ19731FDOQ19731
Author name not available (Why is that?)
Official website: http://research.microsoft.com/en-us/projects/boogie/
Source code repository: https://github.com/boogie-org/boogie
Cited In (only showing first 100 items - show all)
- A learning-based approach to synthesizing invariants for incomplete verification engines
- Heaps and Data Structures: A Challenge for Automated Provers
- Using History Invariants to Verify Observers
- Verifying relative safety, accuracy, and termination for program approximations
- Verifying Whiley programs with Boogie
- Proving mutual termination
- IronFleet
- Checking data-race freedom of GPU kernels, compositionally
- Functional correctness of C implementations of Dijkstra's, Kruskal's, and Prim's algorithms
- Product programs in the wild: retrofitting program verifiers to check information flow security
- Verified cryptographic code for everybody
- Considerate reasoning and the Composite design pattern
- Safe functional systems through integrity types and verified assembly
- Modular verification of procedure equivalence in the presence of memory allocation
- On Bounded Reachability of Programs with Set Comprehensions
- Splitting via Interpolants
- Automated verification of practical garbage collectors
- Title not available (Why is that?)
- Beyond contracts for concurrency
- Program verification by coinduction
- Alloy*: a general-purpose higher-order relational constraint solver
- Deductive verification of floating-point Java programs in KeY
- The relationship between separation logic and implicit dynamic frames
- Fifty years of Hoare's logic
- Horn clause solvers for program verification
- Viper: a verification infrastructure for permission-based reasoning
- A generalised branch-and-bound approach and its application in SAT modulo nonlinear integer arithmetic
- Assertion-based slicing and slice graphs
- Shape analysis of low-level C with overlapping structures
- Automating deductive verification for weak-memory programs
- Loop invariants: analysis, classification, and examples
- Instrumenting a weakest precondition calculus for counterexample generation
- Automating regression verification of pointer programs by predicate abstraction
- On automation in the verification of software barriers: experience report
- Generalized arrays for Stainless frames
- Automated verification of practical garbage collectors
- A verifying compiler for a multi-threaded object-oriented language
- Encoding monomorphic and polymorphic types
- Decision procedures for region logic
- A FOOLish encoding of the next state relations of imperative programs
- Unifying separation logic and region logic to allow interoperability
- Local reasoning for global invariants. II: Dynamic boundaries
- Verification of Higher-Order Computation: A Game-Semantic Approach
- Stepwise refinement of heap-manipulating code in Chalice
- Doomed program points
- Reasoning about memory layouts
- Exploiting pointer analysis in memory models for deductive verification
- Integration of verification methods for program systems
- Automatic proofs of memory deallocation for a Whiley-to-C compiler
- Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach
- Ghidra
- Whiley
- ARQMath
- RustHorn
- SubPolyhedra: A (More) Scalable Approach to Infer Linear Inequalities
- Magic-sets for localised analysis of Java bytecode
- Proving fairness and implementation correctness of a microkernel scheduler
- Relational program reasoning using compiler IR
- A dynamic logic for unstructured programs with embedded assertions
- Invariants synthesis over a combined domain for automated program verification
- The relationship between separation logic and implicit dynamic frames
- Title not available (Why is that?)
- A polymorphic intermediate verification language: design and logical encoding
- An assertional proof of the stability and correctness of Natural Mergesort
- Inferring Loop Invariants Using Postconditions
- HOL-Boogie -- an interactive prover-backend for the verifying C compiler
- The dynamic frames theory
- Wombit: a portfolio bit-vector solver using word-level propagation
- Predicate abstraction in a program logic calculus
- Contract-based verification of MATLAB-style matrix programs
- Automatic verification of Java programs with dynamic frames
- FeatherTrait
- Matching multiplications in bit-vector formulas
- A Basis for Verifying Multi-threaded Programs
- A framework for the verification of certifying computations
- Verification of object-oriented programs: a transformational approach
- First-order automated reasoning with theories: when deduction modulo theory meets practice
- Theorem proving in higher order logics. 21st international conference, TPHOLs 2008, Montreal, Canada, August 18--21, 2008. Proceedings
- Mechanical inference of invariants for FOR-loops
- Behavioral interface specification languages
- Static contract checking with abstract interpretation
- Compositionality Entails Sequentializability
- Verification conditions for source-level imperative programs
- Atoment
- CoqMT
- c2i
- ExplainHoudini
- Houdini
- Looper
- OpenJML
- Goblint
- HAVOC
- Kilim
- LOCKSMITH
- RELAY
- JFlow
- C-Light
- PKind
- CoVaC
- BoogiePL
This page was built for software: Boogie
