The following pages link to Spec# (Q16769):
Displaying 50 items.
- Contract-based verification of MATLAB-style matrix programs (Q282101) (← links)
- Automated verification of shape, size and bag properties via user-defined predicates in separation logic (Q436400) (← links)
- On deciding satisfiability by theorem proving with speculative inferences (Q438533) (← links)
- A sound and complete reasoning system for asynchronous communication with shared futures (Q465485) (← links)
- Fundamentals of software engineering. 6th international conference, FSEN 2015, Tehran, Iran, April 22--24, 2015. Revised selected papers (Q497870) (← links)
- A generic framework for symbolic execution: a coinductive approach (Q507361) (← links)
- Modular inference of subprogram contracts for safety checking (Q604392) (← links)
- Doomed program points (Q633286) (← links)
- Lazy behavioral subtyping (Q710675) (← links)
- A shape graph logic and a shape system (Q744329) (← links)
- Formal verification of a Java component using the RESOLVE framework (Q831953) (← links)
- Automata-based verification of programs with tree updates (Q845236) (← links)
- Contracts for concurrency (Q846109) (← links)
- Beyond contracts for concurrency (Q846113) (← links)
- Towards imperative modules: reasoning about invariants and sharing of mutable state (Q854171) (← links)
- Verification conditions are code (Q855274) (← links)
- Observational purity and encapsulation (Q882452) (← links)
- Automatic verification of Java programs with dynamic frames (Q973055) (← links)
- Refinement and verification in component-based model-driven design (Q1004291) (← links)
- Invariant based programming: Basic approach and teaching experiences (Q1019025) (← links)
- An extensible encoding of object-oriented data models in HOL. With an application to IMP++ (Q1040775) (← links)
- Theory and methodology of assumption/commitment based system interface specification and architectural contracts (Q1654563) (← links)
- Understanding parameters of deductive verification: an empirical investigation of KeY (Q1791175) (← links)
- Unifying separation logic and region logic to allow interoperability (Q1798668) (← links)
- Assertion-based slicing and slice graphs (Q1941855) (← links)
- Stepwise refinement of heap-manipulating code in Chalice (Q1941869) (← links)
- Formal verification of numerical programs: from C annotated programs to mechanical proofs (Q1949765) (← links)
- Modular verification of programs with effects and effects handlers (Q1996433) (← links)
- Verifying Whiley programs with Boogie (Q2102933) (← links)
- Traits: correctness-by-construction for free (Q2165220) (← links)
- Synthesizing precise and useful commutativity conditions (Q2208295) (← links)
- Exploiting pointer analysis in memory models for deductive verification (Q2287078) (← links)
- Verifying data- and control-oriented properties combining static and runtime verification: theory and tools (Q2402555) (← links)
- Formal verification of side-channel countermeasures using self-composition (Q2442950) (← links)
- A proof outline logic for object-oriented programming (Q2571207) (← links)
- Synthesis of positive logic programs for checking a class of definitions with infinite quantification (Q2629858) (← links)
- Are the logical foundations of verifying compiler prototypes matching user expectations? (Q2643125) (← links)
- On assertion-based encapsulation for object invariants and simulations (Q2643129) (← links)
- Specification and verification challenges for sequential object-oriented programs (Q2643131) (← links)
- Faster and more complete extended static checking for the Java modeling language (Q2655328) (← links)
- HOL-Boogie -- an interactive prover-backend for the verifying C compiler (Q2655335) (← links)
- Viper: A Verification Infrastructure for Permission-Based Reasoning (Q2796035) (← links)
- Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach (Q2802468) (← links)
- Model-Based Mutation Testing of Reactive Systems (Q2842624) (← links)
- Invariants Synthesis over a Combined Domain for Automated Program Verification (Q2842643) (← links)
- E-matching for Fun and Profit (Q2864401) (← links)
- From Predicates to Programs: The Semantics of a Method Language (Q2870332) (← links)
- Behavioral interface specification languages (Q2875082) (← links)
- Zeno: An Automated Prover for Properties of Recursive Data Structures (Q2894285) (← links)
- Towards the Formal Specification and Verification of Maple Programs (Q2907326) (← links)
