Boogie

swMATH7714MaRDI QIDQ19731FDOQ19731

Author name not available (Why is that?)

Cited In (only showing first 100 items - show all)

• 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
• Considerate reasoning and the Composite design pattern
• Safe functional systems through integrity types and verified assembly
• Automated Algebraic Reasoning for Collections and Local Variables with Lenses
• Proving the safety of highly-available distributed objects
• Program verification by coinduction
• Principled software development. Essays dedicated to Arnd Poetzsch-Heffter on the occasion of his 60th birthday. Selected papers based on the presentations at the symposium, Kaiserslautern, Germany, November 2018
• 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
• Conjunctive abstract interpretation using paramodulation
• The relationship between separation logic and implicit dynamic frames
• Output-sensitive information flow analysis
• Fifty years of Hoare's logic
• Design and results of the 2nd annual satisfiability modulo theories competition (SMT-COMP 2006)
• Dynamic boundaries: information hiding by second order framing with first order assertions
• Two-level mixed verification method of C-light programs in terms of safety logic
• Shape analysis of low-level C with overlapping structures
• Loop invariants: analysis, classification, and examples
• Time bounds for general function pointers
• Combining model checking and testing
• On automation in the verification of software barriers: experience report
• Generalized arrays for Stainless frames
• Sufficient Preconditions for Modular Assertion Checking
• Decision procedures for region logic
• Verifiable Code Generation from Scheduled Event-B Models
• A FOOLish encoding of the next state relations of imperative programs
• Local reasoning for global invariants. II: Dynamic boundaries
• Verifying Catamorphism-Based Contracts using Constrained Horn Clauses
• Stepwise refinement of heap-manipulating code in Chalice
• Exploiting pointer analysis in memory models for deductive verification
• Automatic proofs of memory deallocation for a Whiley-to-C compiler
• Severity levels of inconsistent code
• Reasoning about loops using Vampire in KeY
• A refinement methodology for object-oriented programs
• ExplainHoudini: making Houdini inference transparent
• Integrated approach to analysis and verification of imperative programs
• Unifying type checking and property checking for low-level code
• Invariants synthesis over a combined domain for automated program verification
• The relationship between separation logic and implicit dynamic frames
• A Machine Checked Soundness Proof for an Intermediate Verification Language
• 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
• 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
• Modular verification of procedure equivalence in the presence of memory allocation
• 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?)
• Beyond contracts for concurrency
• Predicate abstraction in a program logic calculus
• Contract-based verification of MATLAB-style matrix programs
• Automatic verification of Java programs with dynamic frames
• HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier
• Matching multiplications in bit-vector formulas
• A Basis for Verifying Multi-threaded Programs
• Horn clause solvers for program verification
• A framework for the verification of certifying computations
• 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
• Verification of object-oriented programs: a transformational approach
• First-order automated reasoning with theories: when deduction modulo theory meets practice
• 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
• Static contract checking with abstract interpretation
• A verifying compiler for a multi-threaded object-oriented language
• Compositionality Entails Sequentializability
• Verification conditions for source-level imperative programs
• Encoding monomorphic and polymorphic types
• 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

This page was built for software: Boogie