Boogie
From MaRDI portal
Software:19731
swMATH7714MaRDI QIDQ19731FDOQ19731
Author name not available (Why is that?)
Cited In (only showing first 100 items - show all)
- Inferring Loop Invariants Using Postconditions
- Using History Invariants to Verify Observers
- Verifying relative safety, accuracy, and termination for program approximations
- Regression verification for unbalanced recursive functions
- Proving mutual termination
- 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
- Faster and more complete extended static checking for the Java modeling language
- 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
- On Bounded Reachability of Programs with Set Comprehensions
- Automating Induction with an SMT Solver
- Splitting via Interpolants
- Automated verification of practical garbage collectors
- Title not available (Why is that?)
- Zeno: An Automated Prover for Properties of Recursive Data Structures
- Dafny: An Automatic Program Verifier for Functional Correctness
- Beyond contracts for concurrency
- A Dynamic Logic for Unstructured Programs with Embedded Assertions
- Predicate abstraction in a program logic calculus
- Contract-based verification of MATLAB-style matrix programs
- Title not available (Why is that?)
- Automatic verification of Java programs with dynamic frames
- HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier
- A Basis for Verifying Multi-threaded Programs
- A framework for the verification of certifying computations
- Assertion-based slicing and slice graphs
- Verification of object-oriented programs: a transformational approach
- First-order automated reasoning with theories: when deduction modulo theory meets practice
- Modular Verification of Procedure Equivalence in the Presence of Memory Allocation
- Automating deductive verification for weak-memory programs
- 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
- Instrumenting a weakest precondition calculus for counterexample generation
- Behavioral interface specification languages
- Automating regression verification of pointer programs by predicate abstraction
- Automated verification of practical garbage collectors
- Viper: A Verification Infrastructure for Permission-Based Reasoning
- A Generalised Branch-and-Bound Approach and Its Application in SAT Modulo Nonlinear Integer Arithmetic
- Matching Multiplications in Bit-Vector Formulas
- Compositionality Entails Sequentializability
- Horn Clause Solvers for Program Verification
- Verification conditions for source-level imperative programs
- Verification of Concurrent Systems with VerCors
- Why3 — Where Programs Meet Provers
- Interleaving and Lock-Step Semantics for Analysis and Verification of GPU Kernels
- Secure distributed programming with value-dependent types
- A parametric segmentation functor for fully automatic and scalable array content analysis
- Valigator: A Verification Tool with Bound and Invariant Generation
- Unifying separation logic and region logic to allow interoperability
- Verification of Higher-Order Computation: A Game-Semantic Approach
- Doomed program points
- Reasoning about memory layouts
- Integration of verification methods for program systems
- A system for compositional verification of asynchronous objects
- Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach
- An extensible encoding of object-oriented data models in HOL. With an application to IMP++
- SMT proof checking using a logical framework
- SubPolyhedra: A (More) Scalable Approach to Infer Linear Inequalities
- Specification and verification challenges for sequential object-oriented programs
- Magic-sets for localised analysis of Java bytecode
- Static Contract Checking with Abstract Interpretation
- Encoding Monomorphic and Polymorphic Types
- Proving fairness and implementation correctness of a microkernel scheduler
- Predicate Abstraction in a Program Logic Calculus
- Relational program reasoning using compiler IR
- Software engineering and formal methods. 9th international conference, SEFM 2011, Montevideo, Uruguay, November 14--18, 2011. Proceedings
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
- Title not available (Why is that?)
- SMT-based model checking for recursive programs
- A learning-based approach to synthesizing invariants for incomplete verification engines
- Verifying a concurrent garbage collector with a rely-guarantee methodology
- Heaps and Data Structures: A Challenge for Automated Provers
- Verifying Whiley programs with Boogie
- Title not available (Why is that?)
- Loop invariants
- A Refinement Methodology for Object-Oriented Programs
- Safe functional systems through integrity types and verified assembly
- Automated Algebraic Reasoning for Collections and Local Variables with Lenses
- Reasoning About Loops Using Vampire in KeY
- Severity Levels of Inconsistent Code
- Invariants Synthesis over a Combined Domain for Automated Program Verification
- ExplainHoudini: Making Houdini Inference Transparent
- Program verification by coinduction
- Alloy*: a general-purpose higher-order relational constraint solver
- Two for the price of one: lifting separation logic assertions
- Deductive verification of floating-point Java programs in KeY
- The Relationship between Separation Logic and Implicit Dynamic Frames
- Fifty years of Hoare's logic
- Design and results of the 2nd annual satisfiability modulo theories competition (SMT-COMP 2006)
- Local Reasoning for Global Invariants, Part II
- A Polymorphic Intermediate Verification Language: Design and Logical Encoding
- On automation in the verification of software barriers: experience report
- Conjunctive Abstract Interpretation Using Paramodulation
- Generalized arrays for Stainless frames
- Considerate Reasoning and the Composite Design Pattern
- Title not available (Why is that?)
This page was built for software: Boogie