The following pages link to Spec# (Q16769):
Displayed 50 items.
- Effective interactive proofs for higher-order imperative programs (Q2936804) (← links)
- Access permission contracts for scripting languages (Q2942863) (← links)
- (Q2979818) (← links)
- Enforcing Structural Invariants Using Dynamic Frames (Q3000638) (← links)
- Second-Order Programs with Preconditions (Q3058455) (← links)
- Dafny: An Automatic Program Verifier for Functional Correctness (Q3066108) (← links)
- Interleaving Symbolic Execution and Partial Evaluation (Q3066122) (← links)
- CVPP: A Tool Set for Compositional Verification of Control–Flow Safety Properties (Q3067539) (← links)
- A Refinement Methodology for Object-Oriented Programs (Q3067544) (← links)
- ExplainHoudini: Making Houdini Inference Transparent (Q3075491) (← links)
- Hardware-Dependent Proofs of Numerical Programs (Q3100216) (← links)
- WP Semantics and Behavioral Subtyping (Q3105750) (← links)
- Back to the future (Q3189836) (← links)
- Play to Test (Q3434603) (← links)
- Verifying Heap-Manipulating Programs in an SMT Framework (Q3510799) (← links)
- HOL-Boogie — An Interactive Prover for the Boogie Program-Verifier (Q3543656) (← links)
- Hoare type theory, polymorphism and separation (Q3546051) (← links)
- Dynamic Boundaries: Information Hiding by Second Order Framing with First Order Assertions (Q3558212) (← links)
- DKAL and Z3: A Logic Embedding Experiment (Q3586018) (← links)
- A Machine Checked Soundness Proof for an Intermediate Verification Language (Q3599104) (← links)
- Modular Safety Checking for Fine-Grained Concurrency (Q3612005) (← links)
- Verifying Reference Counting Implementations (Q3617768) (← links)
- Abstract Interpretation of Symbolic Execution with Explicit State Updates (Q3638994) (← links)
- An extended account of contract monitoring strategies as patterns of communication (Q4577815) (← links)
- Skill-Based Verification of Cyber-Physical Systems (Q5039533) (← links)
- Holistic Specifications for Robust Programs (Q5039542) (← links)
- RustHorn: CHC-Based Verification for Rust Programs (Q5041108) (← links)
- ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs (Q5041118) (← links)
- Verification of Concurrent Systems with VerCors (Q5175776) (← links)
- Ynot (Q5178765) (← links)
- On Deciding Satisfiability by DPLL( $\Gamma+{\mathcal T}$ ) and Unsound Theorem Proving (Q5191095) (← links)
- Unifying type checking and property checking for low-level code (Q5261528) (← links)
- An Assertional Proof of the Stability and Correctness of Natural Mergesort (Q5277907) (← links)
- Fundamental Approaches to Software Engineering (Q5316436) (← links)
- LMS-Verify: abstraction without regret for verified systems programming (Q5370919) (← links)
- Zap: Automated Theorem Proving for Software Analysis (Q5387827) (← links)
- Sequential, Parallel, and Quantified Updates of First-Order Structures (Q5387908) (← links)
- (Q5389141) (← links)
- Local Reasoning for Global Invariants, Part II (Q5395717) (← links)
- Modular reasoning about heap paths via effectively propositional formulas (Q5408433) (← links)
- A parametric segmentation functor for fully automatic and scalable array content analysis (Q5408536) (← links)
- Verification by Parallelization of Parametric Code (Q5426003) (← links)
- A Representation-Independent Behavioral Semantics for Object-Oriented Components (Q5428910) (← links)
- Using First-Order Theorem Provers in the Jahob Data Structure Verification System (Q5452598) (← links)
- Cibai: An Abstract Interpretation-Based Static Analyzer for Modular Analysis and Verification of Java Classes (Q5452615) (← links)
- Verification of Higher-Order Computation: A Game-Semantic Approach (Q5458405) (← links)
- Semi-persistent Data Structures (Q5458407) (← links)
- A Realizability Model for Impredicative Hoare Type Theory (Q5458408) (← links)
- Programming Languages and Systems (Q5493379) (← links)
- Proving Correctness and Security of Two-Party Computation Implemented in Java in Presence of a Semi-honest Sender (Q5498725) (← links)