ESC/Java
From MaRDI portal
Software:19268
swMATH7217MaRDI QIDQ19268FDOQ19268
Author name not available (Why is that?)
Cited In (only showing first 100 items - show all)
- Loop summarization using state and transition invariants
- Verifying Heap-Manipulating Programs in an SMT Framework
- Tools and Algorithms for the Construction and Analysis of Systems
- Class invariants as abstract interpretation of trace semantics
- Formal methods for smart cards: an experience report
- Inferring Loop Invariants Using Postconditions
- Formalisation and implementation of an algorithm for bytecode verification of \(\@\)NonNull types
- The Daikon system for dynamic detection of likely invariants
- Extended Static Checking by Calculation Using the Pointfree Transform
- Formal verification of a Java component using the RESOLVE framework
- Ghost signals: verifying termination of busy waiting
- Mathematics of Program Construction
- Programming Languages and Systems
- Programming Languages and Systems
- Dynamic inference of polymorphic lock types
- Efficient weakest preconditions
- Faster and more complete extended static checking for the Java modeling language
- HOL-Boogie -- an interactive prover-backend for the verifying C compiler
- A relation-algebraic approach to the ``Hoare logic of functional dependencies
- Automation of broad sanity test generation
- Computer Aided Verification
- Sequential, Parallel, and Quantified Updates of First-Order Structures
- Dafny: An Automatic Program Verifier for Functional Correctness
- Beyond contracts for concurrency
- Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs
- Inferring Sufficient Conditions with Backward Polyhedral Under-Approximations
- Modular Safety Checking for Fine-Grained Concurrency
- Programmed strategies for program verification
- Interpolant Generation for UTVPI
- On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving
- HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier
- Fundamental Approaches to Software Engineering
- Automated verification of shape, size and bag properties via user-defined predicates in separation logic
- On deciding satisfiability by theorem proving with speculative inferences
- Automatic software model checking via constraint logic
- An integrated approach to high integrity software verification
- Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005)
- Model checking, testing and verification working together
- Title not available (Why is that?)
- Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development
- First-order automated reasoning with theories: when deduction modulo theory meets practice
- A Reachability Predicate for Analyzing Low-Level Software
- FM 2005: Formal Methods
- Atomizer: A dynamic atomicity checker for multithreaded programs
- Solving quantified verification conditions using satisfiability modulo theories
- Observational purity and encapsulation
- How the design of JML accommodates both runtime assertion checking and formal verification
- Extending Model Checking with Dynamic Analysis
- A shape graph logic and a shape system
- Model Checking Software
- Title not available (Why is that?)
- Horn Clause Solvers for Program Verification
- A dynamic logic for deductive verification of multi-threaded programs
- Matching Logic: An Alternative to Hoare/Floyd Logic
- Bounded Quantifier Instantiation for Checking Inductive Invariants
- Valigator: A Verification Tool with Bound and Invariant Generation
- Verification, Model Checking, and Abstract Interpretation
- Statically safe program generation with SafeGen
- Weakest pre-condition reasoning for Java programs with JML annotations
- Doomed program points
- Dual analysis for proving safety and finding bugs
- A system for compositional verification of asynchronous objects
- Modular verification of multithreaded programs
- Structural Abstraction of Software Verification Conditions
- Modular verification of programs with effects and effects handlers
- Programming Languages and Systems
- SMT proof checking using a logical framework
- Specification and verification challenges for sequential object-oriented programs
- A mechanical analysis of program verification strategies
- Verification: Theory and Practice
- Title not available (Why is that?)
- Static Contract Checking with Abstract Interpretation
- Programming Languages and Systems
- Frontiers of Combining Systems
- Logical Interpretation: Static Program Analysis Using Theorem Proving
- E-matching for fun and profit
- A proof outline logic for object-oriented programming
- Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories
- Formal Methods for Components and Objects
- Dynamic Model Checking with Property Driven Pruning to Detect Race Conditions
- Tools and Algorithms for the Construction and Analysis of Systems
- Heaps and Data Structures: A Challenge for Automated Provers
- Verifying Reference Counting Implementations
- Verifying Whiley programs with Boogie
- ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs
- Precondition Inference from Intermittent Assertions and Application to Contracts on Collections
- Automating Verification of Loops by Parallelization
- ExplainHoudini: Making Houdini Inference Transparent
- Programming Languages and Systems
- Source code verification of a secure payment applet
- Title not available (Why is that?)
- Two for the price of one: lifting separation logic assertions
- A novel analysis space for pointer analysis and its application for bug finding
- Extended static checking
- Verification by Parallelization of Parametric Code
- Refinement and verification in component-based model-driven design
- WP Semantics and Behavioral Subtyping
- Zap: Automated Theorem Proving for Software Analysis
- A Polymorphic Intermediate Verification Language: Design and Logical Encoding
- A type system for static and dynamic checking of C++ pointers
This page was built for software: ESC/Java
