Cited in
(only showing first 100 items - show all)- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
- Harnessing rCOS for Tool Support —The CoCoME Experience
- A Hoare Logic for Call-by-Value Functional Programs
- Dynamic Model Checking with Property Driven Pruning to Detect Race Conditions
- Formal Methods for Components and Objects
- A polymorphic intermediate verification language: design and logical encoding
- Loop summarization using state and transition invariants
- Verifying Heap-Manipulating Programs in an SMT Framework
- Class invariants as abstract interpretation of trace semantics
- Tools and Algorithms for the Construction and Analysis of Systems
- Verifying Reference Counting Implementations
- Formal methods for smart cards: an experience report
- Tools and Algorithms for the Construction and Analysis of Systems
- WP semantics and behavioral subtyping
- Heaps and Data Structures: A Challenge for Automated Provers
- Formalisation and implementation of an algorithm for bytecode verification of \(\@\)NonNull types
- Inferring Loop Invariants Using Postconditions
- Verifying Whiley programs with Boogie
- Formal verification of a Java component using the RESOLVE framework
- Ghost signals: verifying termination of busy waiting
- The Daikon system for dynamic detection of likely invariants
- Extended Static Checking by Calculation Using the Pointfree Transform
- Dynamic inference of polymorphic lock types
- Mathematics of Program Construction
- Efficient weakest preconditions
- A relation-algebraic approach to the ``Hoare logic of functional dependencies
- Programming Languages and Systems
- Programming Languages and Systems
- Faster and more complete extended static checking for the Java modeling language
- HOL-Boogie -- an interactive prover-backend for the verifying C compiler
- Automation of broad sanity test generation
- Unit checking: symbolic model checking for a unit of code
- Automating Verification of Loops by Parallelization
- Computer Aided Verification
- Beyond contracts for concurrency
- Programming Languages and Systems
- Sequential, Parallel, and Quantified Updates of First-Order Structures
- Source code verification of a secure payment applet
- Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs
- A novel analysis space for pointer analysis and its application for bug finding
- Modular Safety Checking for Fine-Grained Concurrency
- Two for the price of one: lifting separation logic assertions
- Programmed strategies for program verification
- HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier
- Collaborative verification and testing with explicit assumptions
- Interpolant Generation for UTVPI
- On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving
- Extended static checking
- Horn clause solvers for program verification
- Automated verification of shape, size and bag properties via user-defined predicates in separation logic
- On deciding satisfiability by theorem proving with speculative inferences
- Verification by Parallelization of Parametric Code
- An integrated approach to high integrity software verification
- Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005)
- Matching logic: an alternative to Hoare/Floyd logic
- Automatic software model checking via constraint logic
- Bounded quantifier instantiation for checking inductive invariants
- Fundamental Approaches to Software Engineering
- Dynamic boundaries: information hiding by second order framing with first order assertions
- Refinement and verification in component-based model-driven design
- Model checking, testing and verification working together
- scientific article; zbMATH DE number 1956462 (Why is no real title available?)
- First-order automated reasoning with theories: when deduction modulo theory meets practice
- Zap: Automated Theorem Proving for Software Analysis
- Shape analysis of low-level C with overlapping structures
- A type system for static and dynamic checking of C++ pointers
- Atomizer: A dynamic atomicity checker for multithreaded programs
- Are the logical foundations of verifying compiler prototypes matching user expectations?
- Highly dependable concurrent programming using design for verification
- Solving quantified verification conditions using satisfiability modulo theories
- Observational purity and encapsulation
- A Reachability Predicate for Analyzing Low-Level Software
- FM 2005: Formal Methods
- How the design of JML accommodates both runtime assertion checking and formal verification
- Generating error traces from verification-condition counterexamples
- HOL-Boogie
- KeY-C
- Cogent
- jContractor
- Symstra
- rCOS
- LARCH
- SafeGen
- SyncGen
- SCOOP
- BLAST
- KRAKATOA
- SLAM
- SPARK
- Eiffel
- Daikon
- GeoSteiner
- distcc
- Caduceus
- JML
- Omnibus
- Spec#
- IsaWin
- UCLID
- SIMPLIFY
This page was built for software: ESC/Java
