SAT 2015: 18TH INTERNATIONAL CONFERENCE ON THEORY AND APPLICATIONS OF SATISFIABILITY TESTING

This page contains an index consisting of author-provided keywords.

A
Abstract Interpretation	Compositional Recurrence Analysis
Abstraction	Template-based Synthesis of Instruction-Level Abstractions for SoC Verification
Acceleration	Accelerating Invariant Generation
Amortized Analysis	Difference Constraints: An adequate Abstraction for Complexity Analysis of Imperative Programs
arrays	Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays
B
Behavioral Programs	Theory-Aided Model Checking of Concurrent Transition Systems
binary decision diagrams	Universal Boolean Functional Vectors
boolean functional vectors	Universal Boolean Functional Vectors
Boolean Satisfiability	Reverse Engineering with Simulation Graphs
Bound Analysis	Difference Constraints: An adequate Abstraction for Complexity Analysis of Imperative Programs
C
C++ Relaxed Memory Models	Pattern-based Synthesis of Synchronization for the C++ Memory Model
Cache coherence	Verification of Cache Coherence Protocols wrt. Trace Filters
CEGAR algorithm	A CEGAR Algorithm for Generating Skolem Functions from Factored Formulas
Certification	CAQE: A Certifying QBF Solver
circuit transformation	Formal Verification of Automatic Circuit Transformations for Fault-Tolerance
Collision Avoidance	Comparing Different Functional Allocations in Automated Air Traffic Control Design
Complexity Analysis	Difference Constraints: An adequate Abstraction for Complexity Analysis of Imperative Programs
Compositional Analysis	Compositional Recurrence Analysis
compositional reasoning	Compositional Reasoning Gotchas in Practice Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays
Compositional Verification	Theory-Aided Model Checking of Concurrent Transition Systems
concurrent programs	Transaction Flows and Executable Models: Formalization and Analysis of Message passing Protocols
constraint satisfaction problem	Reverse Engineering with Simulation Graphs
Constraint-based program analysis	Compositional Safety Verification with Max-SMT
Coq	Formal Verification of Automatic Circuit Transformations for Fault-Tolerance
CVC4	Theory-Aided Model Checking of Concurrent Transition Systems
D
Difference Constraints	Difference Constraints: An adequate Abstraction for Complexity Analysis of Imperative Programs
digital circuits	Formal Verification of Automatic Circuit Transformations for Fault-Tolerance
distributed protocols	Transaction Flows and Executable Models: Formalization and Analysis of Message passing Protocols
F
factored formula	A CEGAR Algorithm for Generating Skolem Functions from Factored Formulas
Fault Tree Analysis	Comparing Different Functional Allocations in Automated Air Traffic Control Design
fault-tolerance	Formal Verification of Automatic Circuit Transformations for Fault-Tolerance
Firmware	Template-based Synthesis of Instruction-Level Abstractions for SoC Verification
floating point addition	Universal Boolean Functional Vectors
formal methods	IC3 Software Model Checking on Control Flow Automata
formal proofs	Formal Verification of Automatic Circuit Transformations for Fault-Tolerance
Formal Verification	Comparing Different Functional Allocations in Automated Air Traffic Control Design
H
Hardware	Template-based Synthesis of Instruction-Level Abstractions for SoC Verification
hardware verification	Compositional Reasoning Gotchas in Practice Universal Boolean Functional Vectors
horn clauses	Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays
I
IC3	Pushing to the Top
Inductive	IC3 Software Model Checking on Control Flow Automata
Inductive Invariants	Pushing to the Top
Invariant Generation	Accelerating Invariant Generation Compositional Recurrence Analysis
L
Lambdas	Better Lemmas with Lambda Extraction
Lazy Abstraction with Interpolants	Accelerating Invariant Generation
Lemmas on Demand	Better Lemmas with Lambda Extraction
M
memory	Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays
model	Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays
Model Based Safety Assessment	Comparing Different Functional Allocations in Automated Air Traffic Control Design
model checking	Pushing to the Top Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays Transaction Flows and Executable Models: Formalization and Analysis of Message passing Protocols
P
Parameterized Systems	Verification of Cache Coherence Protocols wrt. Trace Filters
parametric representations	Universal Boolean Functional Vectors
PDR	Pushing to the Top
Petri Nets	An SMT-based Approach to Fair Termination Analysis
Q
QBF	CAQE: A Certifying QBF Solver
Quantified Boolean Formulas	CAQE: A Certifying QBF Solver
quantifier elimination	A CEGAR Algorithm for Generating Skolem Functions from Factored Formulas Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays
R
Recurrence Analysis	Compositional Recurrence Analysis
Reverse engineering	Reverse Engineering with Simulation Graphs
S
Safety Properties	Verification of Cache Coherence Protocols wrt. Trace Filters
Safety proving	Compositional Safety Verification with Max-SMT
Satisfiability	CAQE: A Certifying QBF Solver
semantics	Formal Verification of Automatic Circuit Transformations for Fault-Tolerance
Simulation graphs	Reverse Engineering with Simulation Graphs
Skolem function generation	A CEGAR Algorithm for Generating Skolem Functions from Factored Formulas
SMT	Theory-Aided Model Checking of Concurrent Transition Systems Better Lemmas with Lambda Extraction Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays
SMT and Max-SMT	Compositional Safety Verification with Max-SMT
SMT Solver	An SMT-based Approach to Fair Termination Analysis
SoC	Template-based Synthesis of Instruction-Level Abstractions for SoC Verification
soft error	Formal Verification of Automatic Circuit Transformations for Fault-Tolerance
soundness	Compositional Reasoning Gotchas in Practice
Static Analysis	Difference Constraints: An adequate Abstraction for Complexity Analysis of Imperative Programs
Subgraph isomorphism	Reverse Engineering with Simulation Graphs
summary	Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays
Synchronization	Pattern-based Synthesis of Synchronization for the C++ Memory Model
Synthesis	Template-based Synthesis of Instruction-Level Abstractions for SoC Verification Pattern-based Synthesis of Synchronization for the C++ Memory Model Transaction Flows and Executable Models: Formalization and Analysis of Message passing Protocols
T
Termination Analysis	An SMT-based Approach to Fair Termination Analysis
Theory of Arrays	Better Lemmas with Lambda Extraction
Transactional memory	Verification of Cache Coherence Protocols wrt. Trace Filters
V
Verification	IC3 Software Model Checking on Control Flow Automata Template-based Synthesis of Instruction-Level Abstractions for SoC Verification Transaction Flows and Executable Models: Formalization and Analysis of Message passing Protocols
W
Weak Memory Models	Pattern-based Synthesis of Synchronization for the C++ Memory Model

Disclaimer | Powered by EasyChair Smart Program