Boogie

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