swMATH4598MaRDI QIDQ16769FDOQ16769
Author name not available (Why is that?)
Official website: http://dl.acm.org/citation.cfm?id=2131549
Cited In (only showing first 100 items - show all)
- A rewriting logic semantics approach to modular program analysis
- Verifying Heap-Manipulating Programs in an SMT Framework
- A Realizability Model for Impredicative Hoare Type Theory
- LMS-Verify: abstraction without regret for verified systems programming
- Using History Invariants to Verify Observers
- SableJBDD
- Formal verification of a Java component using the RESOLVE framework
- Programming Languages and Systems
- HOL-Boogie -- an interactive prover-backend for the verifying C compiler
- Towards the formal specification and verification of Maple programs
- Sequential, Parallel, and Quantified Updates of First-Order Structures
- BDD
- JDD
- Automata-based verification of programs with tree updates
- Beyond contracts for concurrency
- Contracts for concurrency
- Contract-based verification of MATLAB-style matrix programs
- Automatic verification of Java programs with dynamic frames
- Modular Safety Checking for Fine-Grained Concurrency
- Abstract Interpretation of Symbolic Execution with Explicit State Updates
- Towards imperative modules: reasoning about invariants and sharing of mutable state
- Verification conditions are code
- On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving
- FeatherTrait
- Viper: a verification infrastructure for permission-based reasoning
- Automated verification of shape, size and bag properties via user-defined predicates in separation logic
- On deciding satisfiability by theorem proving with speculative inferences
- Assertion-based slicing and slice graphs
- Refinement and verification in component-based model-driven design
- Using First-Order Theorem Provers in the Jahob Data Structure Verification System
- A Representation-Independent Behavioral Semantics for Object-Oriented Components
- Lazy behavioral subtyping
- Observational purity and encapsulation
- Modular inference of subprogram contracts for safety checking
- Behavioral interface specification languages
- A shape graph logic and a shape system
- Play to Test
- A sound and complete reasoning system for asynchronous communication with shared futures
- Understanding parameters of deductive verification: an empirical investigation of KeY
- Bugs, moles and skeletons: symbolic reasoning for software development
- Crust
- TALx86
- Unifying separation logic and region logic to allow interoperability
- AddressSanitizer
- ANNA
- FreeSpec
- operational
- Local reasoning for global invariants. II: Dynamic boundaries
- CCCC
- Nagini
- Back to the future, revisiting precise program verification using SMT solvers
- Cibai: An Abstract Interpretation-Based Static Analyzer for Modular Analysis and Verification of Java Classes
- Verification of Higher-Order Computation: A Game-Semantic Approach
- Stepwise refinement of heap-manipulating code in Chalice
- Invariant based programming: Basic approach and teaching experiences
- Doomed program points
- Programming Languages and Systems
- Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach
- Modular verification of programs with effects and effects handlers
- An Algebraic Semantics for Contract-Based Software Components
- A generic framework for symbolic execution: a coinductive approach
- Multi-prover verification of floating-point programs
- Specification and verification challenges for sequential object-oriented programs
- Fundamentals of software engineering. 6th international conference, FSEN 2015, Tehran, Iran, April 22--24, 2015. Revised selected papers
- Theory and methodology of assumption/commitment based system interface specification and architectural contracts
- Programming Languages and Systems
- E-matching for fun and profit
- A proof outline logic for object-oriented programming
- Effective interactive proofs for higher-order imperative programs
- Fundamental Approaches to Software Engineering
- On assertion-based encapsulation for object invariants and simulations
- Modular reasoning about heap paths via effectively propositional formulas
- Abstract Predicates and Mutable ADTs in Hoare Type Theory
- Formal verification of numerical programs: from C annotated programs to mechanical proofs
- OCRA
- Hoare type theory, polymorphism and separation
- Faster and more complete extended static checking for the Java modeling language
- HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier
- HOL-Boogie
- IMP++
- Ada95
- ACSL
- distcc
- Caduceus
- JML
- Frama-C
- Omnibus
- Why3
- Alt-Ergo
- cvc3
- SIMPLIFY
- OptiML
- Rascal
- Zap
- Rodin
- ESC/Java
- JUnit
- Pex
- VCC
- JACK
This page was built for software: Spec#
