GLOBAL TALK KEYWORD INDEX

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

# | |

#sat | |

A | |

Abstract Interpretation | |

Abstract State Machines | |

Abstraction | |

Acceleration | |

ACL2 | |

ACL2(r) | |

AIG | |

algorithm configuration | |

Algorithm Portfolios | |

Amortized Analysis | |

Architecture Definition Language | |

arrays | |

assumptions | |

Asynchronous | |

autarky | |

autarky-resolution duality | |

automatic functional instantiation | |

Axiom pinpointing | |

B | |

balance of diversification and intensification | |

BCD | |

BCE | |

bechnmarks | |

Behavioral Programs | |

binary decision diagrams | |

BIP | |

blocked clause elimination | |

Blocked Set | |

boolean functional vectors | |

Boolean Satisfiability | |

Bound Analysis | |

buffers | |

BVA | |

BVE | |

byte-addressed memory | |

C | |

C++ Relaxed Memory Models | |

Cache coherence | |

CDCL | |

CEGAR | |

CEGAR algorithm | |

certificate | |

Certification | |

certification standards | |

Chisel | |

circuit transformation | |

Clause Learning | |

clause processors | |

Clauses | |

clock gating | |

Cloud computing | |

Cluster | |

clustering | |

CNF | |

CNF/DNF formula minimization | |

cnf2aig | |

Codewalker | |

Collision Avoidance | |

combinatorial optimization | |

COMiniSatPS | |

communication fabrics | |

community | |

community structure | |

compiler transformation | |

complex systems | |

Complexity Analysis | |

Compositional | |

Compositional Analysis | |

compositional reasoning | |

Compositional Verification | |

Concepts | |

Concurrency | |

concurrent programs | |

Configuration checking | |

conformance | |

Connecting ACL2 with other systems: SMT solvers | |

constraint satisfaction problem | |

Constraint-based program analysis | |

Context-aware system | |

Control theory | |

convergence | |

Coq | |

correc-by-construction | |

CVC4 | |

Cyber-Physical Systems | |

D | |

data analysis | |

dataflow | |

decision heuristics | |

decision procedures: real arithmetic | |

Decompilation into logic | |

Defeasible reasoning | |

Dependency QBF | |

deployment problem | |

Design-Space Exploration | |

Determinacy | |

Deterministic DNNFs | |

Difference Constraints | |

digital circuits | |

directed reachability | |

distributed protocols | |

distributed systems | |

Divide and Conquer | |

domain-specific language | |

DQBF | |

DRAT | |

E | |

EMA | |

embedded systems | |

Encoding | |

encodings | |

Equivalency | |

Esterel | |

Exponential Moving Average | |

F | |

factored formula | |

Fairness | |

Fault Tree Analysis | |

fault-tolerance | |

Firmware | |

fixed-parameter tractability | |

fixing functions | |

floating point addition | |

Forgetting | |

formal methods | |

Formal modeling | |

formal proofs | |

Formal Verification | |

foundational verification | |

Fourier series formalization | |

FPGA design emulation | |

framework | |

FSM extraction | |

function variables | |

G | |

Gate Detection | |

Glucose | |

Graph Representations | |

graphical models | |

Group-MUS enumeration | |

guards | |

H | |

Hardware | |

Hardware description languages | |

hardware verification | |

Hardware verification: analog/mixed-signal | |

heterogeneous hardware | |

High-Assurance | |

high-level synthesis | |

hitting formulas | |

horn clauses | |

Horn formulae | |

Horn least upper bounds | |

hybrid systems | |

I | |

IC3 | |

identify clause blocks | |

inclusion-exclusion | |

incremental SAT | |

incremental solving | |

Induction | |

Inductive | |

Inductive Invariants | |

Infinite series | |

interpolation | |

Invariant | |

Invariant Generation | |

Ising model | |

K | |

Kahn networks | |

Knowledge Compilation | |

Knowledge compilation and approximation | |

L | |

laissez-faire caching | |

Lambdas | |

large maxsat instances | |

latency-insensitive design | |

Lazy Abstraction with Interpolants | |

lazy grounding | |

learned clause | |

learning | |

Lemmas on Demand | |

levelized SAT solving | |

linear-time analysis | |

Lingeling | |

LLVM | |

Local search | |

Logic optimization with external don't care | |

Loop | |

lower bounds | |

M | |

machine learning | |

MAX-k-CSP | |

MAX-SAT | |

maximal autarky | |

maximum cut | |

Maximum Satisfiability | |

medical software | |

memoization | |

memory | |

memory controller | |

Memory subsystem verification | |

Metric Interval Temporal Logic | |

minimal unsatisfiability | |

Minimal Unsatisfiable Cores | |

minimal unsatisfiable subsets | |

MiniSat | |

model | |

Model Based Safety Assessment | |

model checking | |

model counting | |

model inference | |

Model repair | |

model transformations | |

Model-based development | |

Modeling | |

Multi-agent systems | |

Multi-Rate Systems | |

N | |

nanoelectronics | |

nanophotonics | |

Natural computing | |

Non-clausal formula simplification | |

Non-linear real and integer arithmetic | |

Non-standard analysis | |

nuXmv | |

O | |

online monitoring | |

operational semantics | |

optimization | |

oracles | |

Overspill principle | |

P | |

Parallel | |

Parallel computing | |

parallelization | |

parameter importance | |

parameterized complexity | |

Parameterized Systems | |

parametric representations | |

partial MUS enumeration | |

Partial resolution | |

passive testing | |

PDR | |

perfect numbers | |

performance analysis | |

Petri Nets | |

Portfolio | |

portfolio method | |

power reduction | |

practical analysis | |

prediction | |

Preprocessing | |

production system | |

Program analysis and verification | |

program refinement | |

Programming language design | |

Projection | |

proof assistants | |

Property-based testing | |

propositional satisfiability | |

Pseudo-Boolean | |

Q | |

Q-Resolution | |

QBF | |

QBF proof complexity | |

QF_UF theory | |

quadcopters | |

quantified Boolean formula | |

Quantified Boolean Formulas | |

quantifier | |

quantifier elimination | |

quantum annealing | |

Quine-McCluskey procedure pure SAT-based | |

R | |

reachability | |

reactive systems | |

Real analysis | |

Real-time Systems | |

Recurrence Analysis | |

Redundancy | |

refinement | |

regression | |

Resolution | |

resolution proof analysis | |

Resource Binding | |

Resource Sharing | |

restart | |

Restarts | |

Reverse engineering | |

RTL | |

Rule-based reasoning | |

runtime verification | |

S | |

Safety Properties | |

Safety proving | |

SAFL | |

sampling | |

SAT | |

SAT filter | |

SAT solver | |

SAT solvers | |

SAT solving | |

SAT translation | |

SAT-based algorithms | |

Satisfiability | |

satisfiability algorithm | |

Satisfiability proving | |

SCC-Invariants | |

SCCharts | |

Scenario-Aware Dataflow | |

SCEst | |

second-order logic | |

semantics | |

Sequential Constructiveness | |

series | |

shared memory | |

signal temporal logic | |

Simulation graphs | |

Skolem function generation | |

Skolem functions | |

SMT | |

SMT and Max-SMT | |

SMT Solver | |

SMT solving | |

SoC | |

soft error | |

Software instrumentation | |

Software verification | |

soundness | |

Static Analysis | |

Strategic | |

Stream-processing languages | |

Structure | |

Structured CNFs | |

STS | |

Stuctured instances | |

Subgraph isomorphism | |

sum of products | |

summary | |

SWDiA5BY | |

symbolic execution | |

Synchronization | |

Synchronous Programming | |

Synthesis | |

T | |

TCPAs | |

temporal logic | |

Temporal properties | |

termination | |

Termination Analysis | |

Test bench development | |

theorem proving | |

Theory of Arrays | |

Tiling | |

Tool | |

Toolbox | |

Transactional memory | |

Translation | |

translation validation | |

treewidth | |

type reasoning | |

type safety | |

Type theory | |

U | |

Unsat core | |

UNSAT proof | |

unsatisfiability | |

unsatisfiability proofs | |

Unsatisfiability-based solvers | |

unsatisfiable core | |

V | |

Vacuity | |

Verification | |

Verification & Validation | |

Verification Condition Generation | |

visualisation | |

VMTF | |

VSIDS | |

W | |

Weak Memory Models | |

workload | |

X | |

xMAS | |

Z | |

zenoness |