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

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

#
#sat	(POS15) Model Counting with Arbitrary Alphabets (SAT 2015) Laissez-Faire Caching for Parallel #SAT Solving
A
Abstract Interpretation	(FMCAD15) Compositional Recurrence Analysis
Abstract State Machines	(MEMOCODE'15) Formal validation and verification of a medical software critical component
Abstraction	(MEMOCODE'15) Process algebra semantics and reachability analysis for micro-architectural models of communication fabrics (FMCAD15) Template-based Synthesis of Instruction-Level Abstractions for SoC Verification
Acceleration	(FMCAD15) Accelerating Invariant Generation
ACL2	(ACL2-2015) Second-Order Functions and Theorems in ACL2 (ACL2-2015) A Brief Introduction to Oracle’s Use of ACL2 (ACL2-2015) Reasoning about LLVM code using Codewalker (ACL2-2015) Fix Your Types: A Datatype Definition Library for Unconditional Type Reasoning
ACL2(r)	(ACL2-2015) Fourier Series Formalization in ACL2(r)
AIG	(SAT 2015) Recognition of Nested Gates in CNF Formulas
algorithm configuration	(SAT 2015) SpySMAC: Automated Configuration and Performance Analysis of SAT Solvers
Algorithm Portfolios	(SAT 2015) Search-Space Partitioning for Parallelizing SMT Solvers
Amortized Analysis	(FMCAD15) Difference Constraints: An adequate Abstraction for Complexity Analysis of Imperative Programs
Architecture Definition Language	(MEMOCODE'15) Design and Verification of Multi-Rate Distributed Systems
arrays	(FMCAD15) Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays
assumptions	(SAT 2015) Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API
Asynchronous	(MEMOCODE'15) Compositional design of asynchronous circuits from behavioural concepts
autarky	(SAT 2015) Computing maximal autarkies with few and simple oracle queries
autarky-resolution duality	(SAT 2015) Computing maximal autarkies with few and simple oracle queries
automatic functional instantiation	(ACL2-2015) Second-Order Functions and Theorems in ACL2
Axiom pinpointing	(SAT 2015) Efficient MUS Enumeration of Horn Formulae with Applications to Axiom Pinpointing
B
balance of diversification and intensification	(POS15) Proposal and Application of Search Similarity Index for SAT solver
BCD	(SAT 2015) Recognition of Nested Gates in CNF Formulas
BCE	(SAT 2015) Recognition of Nested Gates in CNF Formulas
bechnmarks	(POS15) Applications of MaxSAT in Data Analysis
Behavioral Programs	(FMCAD15) Theory-Aided Model Checking of Concurrent Transition Systems
binary decision diagrams	(FMCAD15) Universal Boolean Functional Vectors
BIP	(MEMOCODE'15) Optimized Distributed Implementations of Timed Component-based Systems
blocked clause elimination	(SAT 2015) Preprocessing for DQBF
Blocked Set	(SAT 2015) Recognition of Nested Gates in CNF Formulas
boolean functional vectors	(FMCAD15) Universal Boolean Functional Vectors
Boolean Satisfiability	(FMCAD15) Reverse Engineering with Simulation Graphs (SAT 2015) Speeding up MUS Extraction with Preprocessing and Chunking
Bound Analysis	(FMCAD15) Difference Constraints: An adequate Abstraction for Complexity Analysis of Imperative Programs
buffers	(MEMOCODE'15) Implementing Latency-Insensitive Dataflow Blocks
BVA	(SAT 2015) Recognition of Nested Gates in CNF Formulas
BVE	(SAT 2015) Recognition of Nested Gates in CNF Formulas
byte-addressed memory	(ACL2-2015) Stateman: Using Metafunctions to Manage Large Terms Representing Machine States
C
C++ Relaxed Memory Models	(FMCAD15) Pattern-based Synthesis of Synchronization for the C++ Memory Model
Cache coherence	(FMCAD15) Verification of Cache Coherence Protocols wrt. Trace Filters
CDCL	(POS15) Evaluating CDCL Restart Schemes (SAT 2015) Between SAT and UNSAT: The Fundamental Difference in CDCL SAT
CEGAR	(QBF 2015) Skolem functions computation for CEGAR based QBF solvers
CEGAR algorithm	(FMCAD15) A CEGAR Algorithm for Generating Skolem Functions from Factored Formulas
certificate	(QBF 2015) Skolem functions computation for CEGAR based QBF solvers
Certification	(FMCAD15) CAQE: A Certifying QBF Solver
certification standards	(MEMOCODE'15) Formal validation and verification of a medical software critical component
Chisel	(MEMOCODE'15) Layering RTL, SAFL, Handel-C and Bluespec Constructs on Chisel HCL
circuit transformation	(FMCAD15) Formal Verification of Automatic Circuit Transformations for Fault-Tolerance
Clause Learning	(SAT 2015) Using Community Structure to Detect Relevant Learnt Clauses
clause processors	(ACL2-2015) Extending ACL2 with SMT Solvers
Clauses	(SAT 2015) Hints Revealed
clock gating	(MEMOCODE'15) Reducing power with activity trigger analysis
Cloud computing	(SAT 2015) Search-Space Partitioning for Parallelizing SMT Solvers
Cluster	(SAT 2015) HordeSat: A Massively Parallel Portfolio SAT Solver
clustering	(POS15) Applications of MaxSAT in Data Analysis
CNF	(SAT 2015) Recognition of Nested Gates in CNF Formulas
CNF/DNF formula minimization	(SAT 2015) SAT-Based Formula Simplification
cnf2aig	(SAT 2015) Recognition of Nested Gates in CNF Formulas
Codewalker	(ACL2-2015) Reasoning about LLVM code using Codewalker
Collision Avoidance	(FMCAD15) Comparing Different Functional Allocations in Automated Air Traffic Control Design
combinatorial optimization	(POS15) Amoeba-inspired Spatiotemporal Dynamics for Physically Implemented Satisfiability Problem Solvers
COMiniSatPS	(SAT 2015) Between SAT and UNSAT: The Fundamental Difference in CDCL SAT
communication fabrics	(MEMOCODE'15) Process algebra semantics and reachability analysis for micro-architectural models of communication fabrics
community	(POS15) Predicting SAT Solver Performance on Heterogeneous Hardware
community structure	(SAT 2015) Using Community Structure to Detect Relevant Learnt Clauses (SAT 2015) Community Structure Inspired Algorithms for SAT and #SAT (SAT 2015) SATGraf: Visualising the Evolution of SAT Formula Structure in Solvers
compiler transformation	(ACL2-2015) Proving Skipping Refinement with ACL2s
complex systems	(POS15) Amoeba-inspired Spatiotemporal Dynamics for Physically Implemented Satisfiability Problem Solvers
Complexity Analysis	(FMCAD15) Difference Constraints: An adequate Abstraction for Complexity Analysis of Imperative Programs
Compositional	(MEMOCODE'15) Implementing Latency-Insensitive Dataflow Blocks (MEMOCODE'15) Compositional design of asynchronous circuits from behavioural concepts
Compositional Analysis	(FMCAD15) Compositional Recurrence Analysis
compositional reasoning	(FMCAD15) Compositional Reasoning Gotchas in Practice (FMCAD15) Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays
Compositional Verification	(FMCAD15) Theory-Aided Model Checking of Concurrent Transition Systems
Concepts	(MEMOCODE'15) Compositional design of asynchronous circuits from behavioural concepts
Concurrency	(MEMOCODE'15) SCEst: Sequentially Constructive Esterel (MEMOCODE'15) Local and Global Fairness in Concurrent Systems
concurrent programs	(FMCAD15) Transaction Flows and Executable Models: Formalization and Analysis of Message passing Protocols
Configuration checking	(SAT 2015) CCAnr: A Configuration Checking Based Local Search Solver for Non-random Satisfiability
conformance	(MEMOCODE'15) Passive testing of production systems based on model inference
Connecting ACL2 with other systems: SMT solvers	(ACL2-2015) Extending ACL2 with SMT Solvers
constraint satisfaction problem	(FMCAD15) Reverse Engineering with Simulation Graphs (SAT 2015) Constructing SAT filters with a quantum annealer
Constraint-based program analysis	(FMCAD15) Compositional Safety Verification with Max-SMT
Context-aware system	(MEMOCODE'15) Modeling and verifying context-aware non-monotonic reasoning agents
Control theory	(MEMOCODE'15) Local and Global Fairness in Concurrent Systems
convergence	(ACL2-2015) Perfect Numbers in ACL2
Coq	(FMCAD15) Formal Verification of Automatic Circuit Transformations for Fault-Tolerance
correc-by-construction	(MEMOCODE'15) Optimized Distributed Implementations of Timed Component-based Systems
CVC4	(FMCAD15) Theory-Aided Model Checking of Concurrent Transition Systems
Cyber-Physical Systems	(MEMOCODE'15) Modeling Resource Sharing using FSM-SADF
D
data analysis	(POS15) Applications of MaxSAT in Data Analysis
dataflow	(MEMOCODE'15) Implementing Latency-Insensitive Dataflow Blocks
decision heuristics	(SAT 2015) Evaluating CDCL Variable Scoring Schemes
decision procedures: real arithmetic	(ACL2-2015) Extending ACL2 with SMT Solvers
Decompilation into logic	(ACL2-2015) Reasoning about LLVM code using Codewalker
Defeasible reasoning	(MEMOCODE'15) Modeling and verifying context-aware non-monotonic reasoning agents
Dependency QBF	(QBF 2015) Reducing Satisfiability and Reachability to DQBF
deployment problem	(MEMOCODE'15) On the Deployment Problem of Embedded Systems
Design-Space Exploration	(MEMOCODE'15) Modeling Resource Sharing using FSM-SADF
Determinacy	(MEMOCODE'15) SCEst: Sequentially Constructive Esterel
Deterministic DNNFs	(SAT 2015) On Compiling CNFs into Structured Deterministic DNNFs
Difference Constraints	(FMCAD15) Difference Constraints: An adequate Abstraction for Complexity Analysis of Imperative Programs
digital circuits	(FMCAD15) Formal Verification of Automatic Circuit Transformations for Fault-Tolerance
directed reachability	(QBF 2015) Reducing Satisfiability and Reachability to DQBF
distributed protocols	(FMCAD15) Transaction Flows and Executable Models: Formalization and Analysis of Message passing Protocols
distributed systems	(MEMOCODE'15) Optimized Distributed Implementations of Timed Component-based Systems (MEMOCODE'15) Design and Verification of Multi-Rate Distributed Systems
Divide and Conquer	(SAT 2015) Search-Space Partitioning for Parallelizing SMT Solvers
domain-specific language	(MEMOCODE'15) On the Deployment Problem of Embedded Systems
DQBF	(SAT 2015) Preprocessing for DQBF
DRAT	(POS15) Checking Unsatisfiability Proofs in Parallel
E
EMA	(POS15) Evaluating CDCL Restart Schemes
embedded systems	(MEMOCODE'15) On the Deployment Problem of Embedded Systems
Encoding	(SAT 2015) PBLib -- A C++ Toolkit for Encoding Pseudo-Boolean Constraints into CNF
encodings	(POS15) Applications of MaxSAT in Data Analysis
Equivalency	(MEMOCODE'15) Metric Interval Temporal Logic Specification Elicitation and Debugging
Esterel	(MEMOCODE'15) SCEst: Sequentially Constructive Esterel
Exponential Moving Average	(POS15) Evaluating CDCL Restart Schemes
F
factored formula	(FMCAD15) A CEGAR Algorithm for Generating Skolem Functions from Factored Formulas
Fairness	(MEMOCODE'15) Local and Global Fairness in Concurrent Systems
Fault Tree Analysis	(FMCAD15) Comparing Different Functional Allocations in Automated Air Traffic Control Design
fault-tolerance	(FMCAD15) Formal Verification of Automatic Circuit Transformations for Fault-Tolerance
Firmware	(FMCAD15) Template-based Synthesis of Instruction-Level Abstractions for SoC Verification
fixed-parameter tractability	(SAT 2015) Community Structure Inspired Algorithms for SAT and #SAT
fixing functions	(ACL2-2015) Fix Your Types: A Datatype Definition Library for Unconditional Type Reasoning
floating point addition	(FMCAD15) Universal Boolean Functional Vectors
Forgetting	(SAT 2015) Projected Model Counting
formal methods	(ACL2-2015) A Brief Introduction to Oracle’s Use of ACL2 (FMCAD15) IC3 Software Model Checking on Control Flow Automata
Formal modeling	(MEMOCODE'15) Modeling and verifying context-aware non-monotonic reasoning agents
formal proofs	(FMCAD15) Formal Verification of Automatic Circuit Transformations for Fault-Tolerance
Formal Verification	(MEMOCODE'15) Design and Verification of Multi-Rate Distributed Systems (MEMOCODE'15) Towards Verification of Hybrid Systems in a Foundational Proof Assistant (FMCAD15) Comparing Different Functional Allocations in Automated Air Traffic Control Design
foundational verification	(MEMOCODE'15) Towards Verification of Hybrid Systems in a Foundational Proof Assistant
Fourier series formalization	(ACL2-2015) Fourier Series Formalization in ACL2(r)
FPGA design emulation	(MEMOCODE'15) From Signal Temporal Logic to FPGA Monitors
framework	(SAT 2015) Volt: A Lazy Grounding Framework for Solving Very Large MaxSAT Instances
FSM extraction	(MEMOCODE'15) Logic analysis and optimization with quick identification of invariants through one time frame analysis
function variables	(ACL2-2015) Second-Order Functions and Theorems in ACL2
G
Gate Detection	(SAT 2015) Recognition of Nested Gates in CNF Formulas
Glucose	(POS15) Evaluating CDCL Restart Schemes
Graph Representations	(SAT 2015) Exploiting Resolution-based Representations for MaxSAT Solving
graphical models	(POS15) Applications of MaxSAT in Data Analysis
Group-MUS enumeration	(SAT 2015) Efficient MUS Enumeration of Horn Formulae with Applications to Axiom Pinpointing
guards	(ACL2-2015) Fix Your Types: A Datatype Definition Library for Unconditional Type Reasoning
H
Hardware	(MEMOCODE'15) Implementing Latency-Insensitive Dataflow Blocks (FMCAD15) Template-based Synthesis of Instruction-Level Abstractions for SoC Verification
Hardware description languages	(MEMOCODE'15) A Generic Synthesisable Test Bench (MEMOCODE'15) Layering RTL, SAFL, Handel-C and Bluespec Constructs on Chisel HCL
hardware verification	(ACL2-2015) A Brief Introduction to Oracle’s Use of ACL2 (FMCAD15) Compositional Reasoning Gotchas in Practice (FMCAD15) Universal Boolean Functional Vectors
Hardware verification: analog/mixed-signal	(ACL2-2015) Extending ACL2 with SMT Solvers
heterogeneous hardware	(POS15) Predicting SAT Solver Performance on Heterogeneous Hardware
High-Assurance	(MEMOCODE'15) Design and Verification of Multi-Rate Distributed Systems
high-level synthesis	(MEMOCODE'15) C-To-Verilog Translation Validation
hitting formulas	(SAT 2015) Community Structure Inspired Algorithms for SAT and #SAT
horn clauses	(FMCAD15) Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays
Horn formulae	(SAT 2015) Efficient MUS Enumeration of Horn Formulae with Applications to Axiom Pinpointing
Horn least upper bounds	(SAT 2015) SAT-Based Horn Least Upper Bounds
hybrid systems	(MEMOCODE'15) Verification Condition Generation for Hybrid Systems (MEMOCODE'15) Towards Verification of Hybrid Systems in a Foundational Proof Assistant (MEMOCODE'15) From Non-Zenoness Verification to Termination
I
IC3	(FMCAD15) Pushing to the Top
identify clause blocks	(SAT 2015) A New Approach to Partial MUS Enumeration
inclusion-exclusion	(POS15) Model Counting with Arbitrary Alphabets
incremental SAT	(SAT 2015) Mining Implied Literals for Incremental SAT
incremental solving	(SAT 2015) Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API
Induction	(MEMOCODE'15) Logic analysis and optimization with quick identification of invariants through one time frame analysis
Inductive	(FMCAD15) IC3 Software Model Checking on Control Flow Automata
Inductive Invariants	(FMCAD15) Pushing to the Top
Infinite series	(ACL2-2015) Fourier Series Formalization in ACL2(r)
interpolation	(QBF 2015) Feasible Interpolation for QBF Resolution Calculi
Invariant	(MEMOCODE'15) Logic analysis and optimization with quick identification of invariants through one time frame analysis
Invariant Generation	(FMCAD15) Accelerating Invariant Generation (FMCAD15) Compositional Recurrence Analysis
Ising model	(SAT 2015) Constructing SAT filters with a quantum annealer
K
Kahn networks	(MEMOCODE'15) Implementing Latency-Insensitive Dataflow Blocks
Knowledge Compilation	(SAT 2015) On Compiling CNFs into Structured Deterministic DNNFs
Knowledge compilation and approximation	(SAT 2015) SAT-Based Horn Least Upper Bounds
L
laissez-faire caching	(SAT 2015) Laissez-Faire Caching for Parallel #SAT Solving
Lambdas	(FMCAD15) Better Lemmas with Lambda Extraction
large maxsat instances	(SAT 2015) Volt: A Lazy Grounding Framework for Solving Very Large MaxSAT Instances
latency-insensitive design	(MEMOCODE'15) Implementing Latency-Insensitive Dataflow Blocks
Lazy Abstraction with Interpolants	(FMCAD15) Accelerating Invariant Generation
lazy grounding	(SAT 2015) Volt: A Lazy Grounding Framework for Solving Very Large MaxSAT Instances
learned clause	(SAT 2015) Between SAT and UNSAT: The Fundamental Difference in CDCL SAT
learning	(SAT 2015) QELL: QBF Reasoning with Extended Clause Learning and Levelized SAT Solving
Lemmas on Demand	(FMCAD15) Better Lemmas with Lambda Extraction
levelized SAT solving	(SAT 2015) QELL: QBF Reasoning with Extended Clause Learning and Levelized SAT Solving
linear-time analysis	(SAT 2015) Mining Implied Literals for Incremental SAT
Lingeling	(POS15) Evaluating CDCL Restart Schemes
LLVM	(ACL2-2015) Reasoning about LLVM code using Codewalker
Local search	(SAT 2015) CCAnr: A Configuration Checking Based Local Search Solver for Non-random Satisfiability
Logic optimization with external don't care	(MEMOCODE'15) Logic analysis and optimization with quick identification of invariants through one time frame analysis
Loop	(MEMOCODE'15) Symbolic Loop Parallelization for Balancing I/O and Memory Accesses on Processor Arrays
lower bounds	(QBF 2015) Feasible Interpolation for QBF Resolution Calculi
M
machine learning	(MEMOCODE'15) Passive testing of production systems based on model inference
MAX-k-CSP	(SAT 2015) Improved Algorithms for Sparse MAX-SAT and MAX-k-CSP
MAX-SAT	(SAT 2015) Improved Algorithms for Sparse MAX-SAT and MAX-k-CSP
maximal autarky	(SAT 2015) Computing maximal autarkies with few and simple oracle queries
maximum cut	(SAT 2015) Constructing SAT filters with a quantum annealer
Maximum Satisfiability	(POS15) Applications of MaxSAT in Data Analysis (SAT 2015) Exploiting Resolution-based Representations for MaxSAT Solving
medical software	(MEMOCODE'15) Formal validation and verification of a medical software critical component
memoization	(ACL2-2015) Stateman: Using Metafunctions to Manage Large Terms Representing Machine States
memory	(FMCAD15) Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays
memory controller	(ACL2-2015) Proving Skipping Refinement with ACL2s
Memory subsystem verification	(MEMOCODE'15) A Generic Synthesisable Test Bench
Metric Interval Temporal Logic	(MEMOCODE'15) Metric Interval Temporal Logic Specification Elicitation and Debugging
minimal unsatisfiability	(SAT 2015) Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API
Minimal Unsatisfiable Cores	(SAT 2015) Speeding up MUS Extraction with Preprocessing and Chunking
minimal unsatisfiable subsets	(SAT 2015) A New Approach to Partial MUS Enumeration
MiniSat	(SAT 2015) Between SAT and UNSAT: The Fundamental Difference in CDCL SAT
model	(FMCAD15) Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays
Model Based Safety Assessment	(FMCAD15) Comparing Different Functional Allocations in Automated Air Traffic Control Design
model checking	(MEMOCODE'15) Hierarchical Multi-Formalism Proofs of Cyber Physical Systems (MEMOCODE'15) Model and Program Repair via SAT Solving (MEMOCODE'15) Modeling and verifying context-aware non-monotonic reasoning agents (QBF 2015) Reducing Satisfiability and Reachability to DQBF (FMCAD15) Pushing to the Top (FMCAD15) Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays (FMCAD15) Transaction Flows and Executable Models: Formalization and Analysis of Message passing Protocols
model counting	(POS15) Model Counting with Arbitrary Alphabets (SAT 2015) Projected Model Counting (SAT 2015) Community Structure Inspired Algorithms for SAT and #SAT
model inference	(MEMOCODE'15) Passive testing of production systems based on model inference
Model repair	(MEMOCODE'15) Model and Program Repair via SAT Solving
model transformations	(MEMOCODE'15) Optimized Distributed Implementations of Timed Component-based Systems
Model-based development	(MEMOCODE'15) Hierarchical Multi-Formalism Proofs of Cyber Physical Systems
Modeling	(MEMOCODE'15) Modeling Resource Sharing using FSM-SADF
Multi-agent systems	(MEMOCODE'15) Modeling and verifying context-aware non-monotonic reasoning agents
Multi-Rate Systems	(MEMOCODE'15) Design and Verification of Multi-Rate Distributed Systems
N
nanoelectronics	(POS15) Amoeba-inspired Spatiotemporal Dynamics for Physically Implemented Satisfiability Problem Solvers
nanophotonics	(POS15) Amoeba-inspired Spatiotemporal Dynamics for Physically Implemented Satisfiability Problem Solvers
Natural computing	(POS15) Amoeba-inspired Spatiotemporal Dynamics for Physically Implemented Satisfiability Problem Solvers
Non-clausal formula simplification	(SAT 2015) SAT-Based Formula Simplification
Non-linear real and integer arithmetic	(SAT 2015) SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving
Non-standard analysis	(ACL2-2015) Fourier Series Formalization in ACL2(r)
nuXmv	(MEMOCODE'15) Process algebra semantics and reachability analysis for micro-architectural models of communication fabrics
O
online monitoring	(MEMOCODE'15) From Signal Temporal Logic to FPGA Monitors
operational semantics	(ACL2-2015) Stateman: Using Metafunctions to Manage Large Terms Representing Machine States
optimization	(MEMOCODE'15) On the Deployment Problem of Embedded Systems
oracles	(SAT 2015) Computing maximal autarkies with few and simple oracle queries
Overspill principle	(ACL2-2015) Fourier Series Formalization in ACL2(r)
P
Parallel	(SAT 2015) SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving (SAT 2015) HordeSat: A Massively Parallel Portfolio SAT Solver
Parallel computing	(SAT 2015) Search-Space Partitioning for Parallelizing SMT Solvers
parallelization	(POS15) Checking Unsatisfiability Proofs in Parallel (MEMOCODE'15) Symbolic Loop Parallelization for Balancing I/O and Memory Accesses on Processor Arrays (SAT 2015) Laissez-Faire Caching for Parallel #SAT Solving
parameter importance	(SAT 2015) SpySMAC: Automated Configuration and Performance Analysis of SAT Solvers
parameterized complexity	(SAT 2015) Community Structure Inspired Algorithms for SAT and #SAT
Parameterized Systems	(FMCAD15) Verification of Cache Coherence Protocols wrt. Trace Filters
parametric representations	(FMCAD15) Universal Boolean Functional Vectors
partial MUS enumeration	(SAT 2015) A New Approach to Partial MUS Enumeration
Partial resolution	(SAT 2015) Hints Revealed
passive testing	(MEMOCODE'15) Passive testing of production systems based on model inference
PDR	(FMCAD15) Pushing to the Top
perfect numbers	(ACL2-2015) Perfect Numbers in ACL2
performance analysis	(SAT 2015) SpySMAC: Automated Configuration and Performance Analysis of SAT Solvers
Petri Nets	(FMCAD15) An SMT-based Approach to Fair Termination Analysis
Portfolio	(SAT 2015) HordeSat: A Massively Parallel Portfolio SAT Solver
portfolio method	(POS15) Proposal and Application of Search Similarity Index for SAT solver
power reduction	(MEMOCODE'15) Reducing power with activity trigger analysis
practical analysis	(SAT 2015) A New Approach to Partial MUS Enumeration
prediction	(POS15) Predicting SAT Solver Performance on Heterogeneous Hardware
Preprocessing	(SAT 2015) Speeding up MUS Extraction with Preprocessing and Chunking (SAT 2015) Preprocessing for DQBF (SAT 2015) Recognition of Nested Gates in CNF Formulas
production system	(MEMOCODE'15) Passive testing of production systems based on model inference
Program analysis and verification	(MEMOCODE'15) Towards Refinement Types for Time-Dependent Data-Flow Networks
program refinement	(ACL2-2015) Second-Order Functions and Theorems in ACL2
Programming language design	(MEMOCODE'15) Towards Refinement Types for Time-Dependent Data-Flow Networks
Projection	(SAT 2015) Projected Model Counting
proof assistants	(MEMOCODE'15) Towards Verification of Hybrid Systems in a Foundational Proof Assistant
Property-based testing	(MEMOCODE'15) A Generic Synthesisable Test Bench
propositional satisfiability	(SAT 2015) Between SAT and UNSAT: The Fundamental Difference in CDCL SAT
Pseudo-Boolean	(SAT 2015) PBLib -- A C++ Toolkit for Encoding Pseudo-Boolean Constraints into CNF
Q
Q-Resolution	(QBF 2015) Feasible Interpolation for QBF Resolution Calculi
QBF	(QBF 2015) Skolem functions computation for CEGAR based QBF solvers (FMCAD15) CAQE: A Certifying QBF Solver (SAT 2015) Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API
QBF proof complexity	(QBF 2015) Feasible Interpolation for QBF Resolution Calculi
QF_UF theory	(SAT 2015) Search-Space Partitioning for Parallelizing SMT Solvers
quadcopters	(MEMOCODE'15) Towards Verification of Hybrid Systems in a Foundational Proof Assistant
quantified Boolean formula	(MEMOCODE'15) Logic analysis and optimization with quick identification of invariants through one time frame analysis (SAT 2015) QELL: QBF Reasoning with Extended Clause Learning and Levelized SAT Solving (SAT 2015) Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API
Quantified Boolean Formulas	(FMCAD15) CAQE: A Certifying QBF Solver
quantifier	(QBF 2015) Skolem functions computation for CEGAR based QBF solvers
quantifier elimination	(FMCAD15) A CEGAR Algorithm for Generating Skolem Functions from Factored Formulas (FMCAD15) Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays
quantum annealing	(SAT 2015) Constructing SAT filters with a quantum annealer
Quine-McCluskey procedure pure SAT-based	(SAT 2015) SAT-Based Formula Simplification
R
reachability	(MEMOCODE'15) Process algebra semantics and reachability analysis for micro-architectural models of communication fabrics
reactive systems	(ACL2-2015) Proving Skipping Refinement with ACL2s
Real analysis	(ACL2-2015) Fourier Series Formalization in ACL2(r)
Real-time Systems	(MEMOCODE'15) Optimized Distributed Implementations of Timed Component-based Systems (MEMOCODE'15) Design and Verification of Multi-Rate Distributed Systems
Recurrence Analysis	(FMCAD15) Compositional Recurrence Analysis
Redundancy	(MEMOCODE'15) Metric Interval Temporal Logic Specification Elicitation and Debugging
refinement	(ACL2-2015) Proving Skipping Refinement with ACL2s
regression	(POS15) Predicting SAT Solver Performance on Heterogeneous Hardware
Resolution	(SAT 2015) Hints Revealed
resolution proof analysis	(SAT 2015) Mining Implied Literals for Incremental SAT
Resource Binding	(MEMOCODE'15) Modeling Resource Sharing using FSM-SADF
Resource Sharing	(MEMOCODE'15) Modeling Resource Sharing using FSM-SADF
restart	(SAT 2015) Between SAT and UNSAT: The Fundamental Difference in CDCL SAT
Restarts	(POS15) Evaluating CDCL Restart Schemes
Reverse engineering	(FMCAD15) Reverse Engineering with Simulation Graphs
RTL	(MEMOCODE'15) Reducing power with activity trigger analysis
Rule-based reasoning	(MEMOCODE'15) Modeling and verifying context-aware non-monotonic reasoning agents
runtime verification	(MEMOCODE'15) From Signal Temporal Logic to FPGA Monitors (MEMOCODE'15) Automatic and Configurable Instrumentation of C Programs with Temporal Assertion Checkers
S
Safety Properties	(FMCAD15) Verification of Cache Coherence Protocols wrt. Trace Filters
Safety proving	(FMCAD15) Compositional Safety Verification with Max-SMT
SAFL	(MEMOCODE'15) Layering RTL, SAFL, Handel-C and Bluespec Constructs on Chisel HCL
sampling	(SAT 2015) Constructing SAT filters with a quantum annealer
SAT	(POS15) Predicting SAT Solver Performance on Heterogeneous Hardware (POS15) Evaluating CDCL Restart Schemes (QBF 2015) Reducing Satisfiability and Reachability to DQBF (SAT 2015) Evaluating CDCL Variable Scoring Schemes (SAT 2015) Community Structure Inspired Algorithms for SAT and #SAT (SAT 2015) Between SAT and UNSAT: The Fundamental Difference in CDCL SAT (SAT 2015) SATGraf: Visualising the Evolution of SAT Formula Structure in Solvers
SAT filter	(SAT 2015) Constructing SAT filters with a quantum annealer
SAT solver	(POS15) Proposal and Application of Search Similarity Index for SAT solver (SAT 2015) CCAnr: A Configuration Checking Based Local Search Solver for Non-random Satisfiability
SAT solvers	(SAT 2015) Using Community Structure to Detect Relevant Learnt Clauses
SAT solving	(MEMOCODE'15) Model and Program Repair via SAT Solving
SAT translation	(SAT 2015) Computing maximal autarkies with few and simple oracle queries
SAT-based algorithms	(SAT 2015) SAT-Based Horn Least Upper Bounds
Satisfiability	(MEMOCODE'15) Metric Interval Temporal Logic Specification Elicitation and Debugging (QBF 2015) Reducing Satisfiability and Reachability to DQBF (FMCAD15) CAQE: A Certifying QBF Solver (SAT 2015) HordeSat: A Massively Parallel Portfolio SAT Solver
satisfiability algorithm	(SAT 2015) Improved Algorithms for Sparse MAX-SAT and MAX-k-CSP
Satisfiability proving	(SAT 2015) Hints Revealed
SCC-Invariants	(MEMOCODE'15) Verification Condition Generation for Hybrid Systems
SCCharts	(MEMOCODE'15) SCEst: Sequentially Constructive Esterel
Scenario-Aware Dataflow	(MEMOCODE'15) Modeling Resource Sharing using FSM-SADF
SCEst	(MEMOCODE'15) SCEst: Sequentially Constructive Esterel
second-order logic	(ACL2-2015) Second-Order Functions and Theorems in ACL2
semantics	(FMCAD15) Formal Verification of Automatic Circuit Transformations for Fault-Tolerance
Sequential Constructiveness	(MEMOCODE'15) SCEst: Sequentially Constructive Esterel
series	(ACL2-2015) Perfect Numbers in ACL2
shared memory	(SAT 2015) Laissez-Faire Caching for Parallel #SAT Solving
signal temporal logic	(MEMOCODE'15) Metric Interval Temporal Logic Specification Elicitation and Debugging (MEMOCODE'15) From Signal Temporal Logic to FPGA Monitors
Simulation graphs	(FMCAD15) Reverse Engineering with Simulation Graphs
Skolem function generation	(FMCAD15) A CEGAR Algorithm for Generating Skolem Functions from Factored Formulas
Skolem functions	(QBF 2015) Skolem functions computation for CEGAR based QBF solvers
SMT	(FMCAD15) Theory-Aided Model Checking of Concurrent Transition Systems (FMCAD15) Better Lemmas with Lambda Extraction (FMCAD15) Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays (SAT 2015) Search-Space Partitioning for Parallelizing SMT Solvers
SMT and Max-SMT	(FMCAD15) Compositional Safety Verification with Max-SMT
SMT Solver	(FMCAD15) An SMT-based Approach to Fair Termination Analysis
SMT solving	(SAT 2015) SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving
SoC	(FMCAD15) Template-based Synthesis of Instruction-Level Abstractions for SoC Verification
soft error	(FMCAD15) Formal Verification of Automatic Circuit Transformations for Fault-Tolerance
Software instrumentation	(MEMOCODE'15) Automatic and Configurable Instrumentation of C Programs with Temporal Assertion Checkers
Software verification	(ACL2-2015) Reasoning about LLVM code using Codewalker
soundness	(FMCAD15) Compositional Reasoning Gotchas in Practice
Static Analysis	(FMCAD15) Difference Constraints: An adequate Abstraction for Complexity Analysis of Imperative Programs
Strategic	(SAT 2015) SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving
Stream-processing languages	(MEMOCODE'15) Towards Refinement Types for Time-Dependent Data-Flow Networks
Structure	(SAT 2015) Recognition of Nested Gates in CNF Formulas
Structured CNFs	(SAT 2015) On Compiling CNFs into Structured Deterministic DNNFs
STS	(MEMOCODE'15) Passive testing of production systems based on model inference
Stuctured instances	(SAT 2015) CCAnr: A Configuration Checking Based Local Search Solver for Non-random Satisfiability
Subgraph isomorphism	(FMCAD15) Reverse Engineering with Simulation Graphs
sum of products	(SAT 2015) Community Structure Inspired Algorithms for SAT and #SAT
summary	(FMCAD15) Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays
SWDiA5BY	(SAT 2015) Between SAT and UNSAT: The Fundamental Difference in CDCL SAT
symbolic execution	(ACL2-2015) Stateman: Using Metafunctions to Manage Large Terms Representing Machine States
Synchronization	(FMCAD15) Pattern-based Synthesis of Synchronization for the C++ Memory Model
Synchronous Programming	(MEMOCODE'15) SCEst: Sequentially Constructive Esterel
Synthesis	(FMCAD15) Template-based Synthesis of Instruction-Level Abstractions for SoC Verification (FMCAD15) Pattern-based Synthesis of Synchronization for the C++ Memory Model (FMCAD15) Transaction Flows and Executable Models: Formalization and Analysis of Message passing Protocols
T
TCPAs	(MEMOCODE'15) Symbolic Loop Parallelization for Balancing I/O and Memory Accesses on Processor Arrays
temporal logic	(MEMOCODE'15) Towards Verification of Hybrid Systems in a Foundational Proof Assistant
Temporal properties	(MEMOCODE'15) Automatic and Configurable Instrumentation of C Programs with Temporal Assertion Checkers
termination	(MEMOCODE'15) From Non-Zenoness Verification to Termination
Termination Analysis	(FMCAD15) An SMT-based Approach to Fair Termination Analysis
Test bench development	(MEMOCODE'15) A Generic Synthesisable Test Bench
theorem proving	(ACL2-2015) A Brief Introduction to Oracle’s Use of ACL2
Theory of Arrays	(FMCAD15) Better Lemmas with Lambda Extraction
Tiling	(MEMOCODE'15) Symbolic Loop Parallelization for Balancing I/O and Memory Accesses on Processor Arrays
Tool	(SAT 2015) PBLib -- A C++ Toolkit for Encoding Pseudo-Boolean Constraints into CNF
Toolbox	(SAT 2015) SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving
Transactional memory	(FMCAD15) Verification of Cache Coherence Protocols wrt. Trace Filters
Translation	(MEMOCODE'15) Hierarchical Multi-Formalism Proofs of Cyber Physical Systems
translation validation	(MEMOCODE'15) C-To-Verilog Translation Validation
treewidth	(SAT 2015) Community Structure Inspired Algorithms for SAT and #SAT
type reasoning	(ACL2-2015) Fix Your Types: A Datatype Definition Library for Unconditional Type Reasoning
type safety	(ACL2-2015) Fix Your Types: A Datatype Definition Library for Unconditional Type Reasoning
Type theory	(MEMOCODE'15) Towards Refinement Types for Time-Dependent Data-Flow Networks
U
Unsat core	(SAT 2015) Hints Revealed
UNSAT proof	(SAT 2015) Between SAT and UNSAT: The Fundamental Difference in CDCL SAT
unsatisfiability	(SAT 2015) A New Approach to Partial MUS Enumeration
unsatisfiability proofs	(POS15) Checking Unsatisfiability Proofs in Parallel
Unsatisfiability-based solvers	(SAT 2015) Exploiting Resolution-based Representations for MaxSAT Solving
unsatisfiable core	(SAT 2015) Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API
V
Vacuity	(MEMOCODE'15) Metric Interval Temporal Logic Specification Elicitation and Debugging
Verification	(MEMOCODE'15) Local and Global Fairness in Concurrent Systems (MEMOCODE'15) Hierarchical Multi-Formalism Proofs of Cyber Physical Systems (MEMOCODE'15) C-To-Verilog Translation Validation (FMCAD15) IC3 Software Model Checking on Control Flow Automata (FMCAD15) Template-based Synthesis of Instruction-Level Abstractions for SoC Verification (FMCAD15) Transaction Flows and Executable Models: Formalization and Analysis of Message passing Protocols
Verification & Validation	(MEMOCODE'15) Formal validation and verification of a medical software critical component
Verification Condition Generation	(MEMOCODE'15) Verification Condition Generation for Hybrid Systems
visualisation	(SAT 2015) SATGraf: Visualising the Evolution of SAT Formula Structure in Solvers
VMTF	(SAT 2015) Evaluating CDCL Variable Scoring Schemes
VSIDS	(SAT 2015) Evaluating CDCL Variable Scoring Schemes (SAT 2015) Between SAT and UNSAT: The Fundamental Difference in CDCL SAT
W
Weak Memory Models	(FMCAD15) Pattern-based Synthesis of Synchronization for the C++ Memory Model
workload	(SAT 2015) A New Approach to Partial MUS Enumeration
X
xMAS	(MEMOCODE'15) Process algebra semantics and reachability analysis for micro-architectural models of communication fabrics
Z
zenoness	(MEMOCODE'15) From Non-Zenoness Verification to Termination

Disclaimer | Powered by EasyChair Smart Program