Linked e-resources
Details
Table of Contents
SMT Techniques and Applications
POLING: SMT Aided Linearizability Proofs
Finding Bounded Path in Graph Using SMT for Automatic Clock Routing
Cutting the Mix
The Inez Mathematical Programming Modulo Theories Framework
Using Minimal Correction Sets to More Efficiently Compute Minimal Unsatisfiable Sets
Deciding Local Theory Extensions via E-matching
HW Verification
Modular Deductive Verification of Multiprocessor Hardware Designs
Word-Level Symbolic Trajectory Evaluation
Verifying Linearizability of Intel® Software Guard Extensions
Synthesis Synthesis Through Unification
From Non-preemptive to Preemptive Scheduling Using Synchronization Synthesis
Counterexample-Guided Quantifier Instantiation for Synthesis in SMT
Deductive Program Repair
Quantifying Conformance Using the Skorokhod Metric
Pareto Curves of Multidimensional Mean-Payoff Games
Termination
Conflict-Driven Conditional Termination
Predicate Abstraction and CEGAR for Disproving Termination of Higher-Order Functional Programs
Complexity of Bradley-Manna-Sipma Lexicographic Ranking Functions
Measuring with Timed Patterns
Automatic Verification of Stability and Safety for Delay Differential Equations
Time Robustness in MTL and Expressivity in Hybrid System Falsification
Concurrency
Adaptive Concretization for Parallel Program Synthesis
Automatic Completion of Distributed Protocols with Symmetry
An Axiomatic Specification for Sequential Memory Models
Approximate Synchrony: An Abstraction for Distributed Almost-Synchronous Systems
Automated and Modular Refinement Reasoning for Concurrent Programs.
POLING: SMT Aided Linearizability Proofs
Finding Bounded Path in Graph Using SMT for Automatic Clock Routing
Cutting the Mix
The Inez Mathematical Programming Modulo Theories Framework
Using Minimal Correction Sets to More Efficiently Compute Minimal Unsatisfiable Sets
Deciding Local Theory Extensions via E-matching
HW Verification
Modular Deductive Verification of Multiprocessor Hardware Designs
Word-Level Symbolic Trajectory Evaluation
Verifying Linearizability of Intel® Software Guard Extensions
Synthesis Synthesis Through Unification
From Non-preemptive to Preemptive Scheduling Using Synchronization Synthesis
Counterexample-Guided Quantifier Instantiation for Synthesis in SMT
Deductive Program Repair
Quantifying Conformance Using the Skorokhod Metric
Pareto Curves of Multidimensional Mean-Payoff Games
Termination
Conflict-Driven Conditional Termination
Predicate Abstraction and CEGAR for Disproving Termination of Higher-Order Functional Programs
Complexity of Bradley-Manna-Sipma Lexicographic Ranking Functions
Measuring with Timed Patterns
Automatic Verification of Stability and Safety for Delay Differential Equations
Time Robustness in MTL and Expressivity in Hybrid System Falsification
Concurrency
Adaptive Concretization for Parallel Program Synthesis
Automatic Completion of Distributed Protocols with Symmetry
An Axiomatic Specification for Sequential Memory Models
Approximate Synchrony: An Abstraction for Distributed Almost-Synchronous Systems
Automated and Modular Refinement Reasoning for Concurrent Programs.