ESC/Java

swMATH7217MaRDI QIDQ19268

No author found.

Related Items (only showing first 100 items - show all)

Unnamed Item ⋮ Unnamed Item ⋮ Tools and Algorithms for the Construction and Analysis of Systems ⋮ Computer Aided Verification ⋮ Automated Technology for Verification and Analysis ⋮ Sequential, Parallel, and Quantified Updates of First-Order Structures ⋮ FM 2005: Formal Methods ⋮ Programming Languages and Systems ⋮ Frontiers of Combining Systems ⋮ Proving Programs Incorrect Using a Sequent Calculus for Java Dynamic Logic ⋮ Verification by Parallelization of Parametric Code ⋮ Structural Abstraction of Software Verification Conditions ⋮ Bugs, Moles and Skeletons: Symbolic Reasoning for Software Development ⋮ A Reachability Predicate for Analyzing Low-Level Software ⋮ Extending Model Checking with Dynamic Analysis ⋮ Programming Languages and Systems ⋮ Programming Languages and Systems ⋮ Model Checking Software ⋮ Verification, Model Checking, and Abstract Interpretation ⋮ Valigator: A Verification Tool with Bound and Invariant Generation ⋮ ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs ⋮ Weakest pre-condition reasoning for Java programs with JML annotations ⋮ Source code verification of a secure payment applet ⋮ Formal verification of a Java component using the RESOLVE framework ⋮ Ghost signals: verifying termination of busy waiting ⋮ Efficient weakest preconditions ⋮ Cooperative bug isolation. Winning thesis of the 2005 ACM doctoral dissertation competition. ⋮ Automatic software model checking via constraint logic ⋮ Automation of broad sanity test generation ⋮ Beyond contracts for concurrency ⋮ Verification: Theory and Practice ⋮ Two for the Price of One: Lifting Separation Logic Assertions ⋮ Are the logical foundations of verifying compiler prototypes matching user expectations? ⋮ Highly dependable concurrent programming using design for verification ⋮ Specification and verification challenges for sequential object-oriented programs ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Mathematics of Program Construction ⋮ Mathematics of Program Construction ⋮ Design and results of the first satisfiability modulo theories competition (SMT-COMP 2005) ⋮ An integrated approach to high integrity software verification ⋮ Concurrency bugs in multithreaded software: modeling and analysis using Petri nets ⋮ Faster and more complete extended static checking for the Java modeling language ⋮ HOL-Boogie -- an interactive prover-backend for the verifying C compiler ⋮ Verifying data- and control-oriented properties combining static and runtime verification: theory and tools ⋮ Observational purity and encapsulation ⋮ Horn Clause Solvers for Program Verification ⋮ Unnamed Item ⋮ A graph-based generic type system for object-oriented programs ⋮ A relation-algebraic approach to the ``Hoare logic of functional dependencies ⋮ Verifying Heap-Manipulating Programs in an SMT Framework ⋮ Unnamed Item ⋮ Doomed program points ⋮ Automated verification of shape, size and bag properties via user-defined predicates in separation logic ⋮ On deciding satisfiability by theorem proving with speculative inferences ⋮ A Hoare Logic for Call-by-Value Functional Programs ⋮ A system for compositional verification of asynchronous objects ⋮ Dual analysis for proving safety and finding bugs ⋮ First-order automated reasoning with theories: when deduction modulo theory meets practice ⋮ Harnessing rCOS for Tool Support —The CoCoME Experience ⋮ SMT proof checking using a logical framework ⋮ Atomizer: A dynamic atomicity checker for multithreaded programs ⋮ Dynamic Model Checking with Property Driven Pruning to Detect Race Conditions ⋮ A dynamic logic for deductive verification of multi-threaded programs ⋮ A mechanical analysis of program verification strategies ⋮ Unnamed Item ⋮ Zap: Automated Theorem Proving for Software Analysis ⋮ Automating Verification of Loops by Parallelization ⋮ HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier ⋮ Bounded Quantifier Instantiation for Checking Inductive Invariants ⋮ The Daikon system for dynamic detection of likely invariants ⋮ A Polymorphic Intermediate Verification Language: Design and Logical Encoding ⋮ Dynamic Boundaries: Information Hiding by Second Order Framing with First Order Assertions ⋮ Collaborative Verification and Testing with Explicit Assumptions ⋮ Class invariants as abstract interpretation of trace semantics ⋮ Loop summarization using state and transition invariants ⋮ Modular verification of programs with effects and effects handlers ⋮ Applying Light-Weight Theorem Proving to Debugging and Verifying Pointer Programs ⋮ Unnamed Item ⋮ Statically safe program generation with SafeGen ⋮ Formalisation and implementation of an algorithm for bytecode verification of \(\@\)NonNull types ⋮ Inferring Sufficient Conditions with Backward Polyhedral Under-Approximations ⋮ Inferring Loop Invariants Using Postconditions ⋮ A type system for static and dynamic checking of C++ pointers ⋮ Modular verification of multithreaded programs ⋮ Orion: High-Precision Methods for Static Error Analysis of C and C++ Programs ⋮ Formal methods for smart cards: an experience report ⋮ How the design of JML accommodates both runtime assertion checking and formal verification ⋮ Generating error traces from verification-condition counterexamples ⋮ Extended Static Checking by Calculation Using the Pointfree Transform ⋮ On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving ⋮ Interpolant Generation for UTVPI ⋮ A novel analysis space for pointer analysis and its application for bug finding ⋮ Logical Interpretation: Static Program Analysis Using Theorem Proving ⋮ Heaps and Data Structures: A Challenge for Automated Provers ⋮ Modular Safety Checking for Fine-Grained Concurrency ⋮ Dafny: An Automatic Program Verifier for Functional Correctness ⋮ Matching Logic: An Alternative to Hoare/Floyd Logic ⋮ Static Contract Checking with Abstract Interpretation ⋮ Verifying Reference Counting Implementations

This page was built for software: ESC/Java