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

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

A
Abstract State Machines	Formal validation and verification of a medical software critical component
Abstraction	Process algebra semantics and reachability analysis for micro-architectural models of communication fabrics
Architecture Definition Language	Design and Verification of Multi-Rate Distributed Systems
Asynchronous	Compositional design of asynchronous circuits from behavioural concepts
B
BIP	Optimized Distributed Implementations of Timed Component-based Systems
buffers	Implementing Latency-Insensitive Dataflow Blocks
C
certification standards	Formal validation and verification of a medical software critical component
Chisel	Layering RTL, SAFL, Handel-C and Bluespec Constructs on Chisel HCL
clock gating	Reducing power with activity trigger analysis
communication fabrics	Process algebra semantics and reachability analysis for micro-architectural models of communication fabrics
Compositional	Implementing Latency-Insensitive Dataflow Blocks Compositional design of asynchronous circuits from behavioural concepts
Concepts	Compositional design of asynchronous circuits from behavioural concepts
Concurrency	SCEst: Sequentially Constructive Esterel Local and Global Fairness in Concurrent Systems
conformance	Passive testing of production systems based on model inference
Context-aware system	Modeling and verifying context-aware non-monotonic reasoning agents
Control theory	Local and Global Fairness in Concurrent Systems
correc-by-construction	Optimized Distributed Implementations of Timed Component-based Systems
Cyber-Physical Systems	Modeling Resource Sharing using FSM-SADF
D
dataflow	Implementing Latency-Insensitive Dataflow Blocks
Defeasible reasoning	Modeling and verifying context-aware non-monotonic reasoning agents
deployment problem	On the Deployment Problem of Embedded Systems
Design-Space Exploration	Modeling Resource Sharing using FSM-SADF
Determinacy	SCEst: Sequentially Constructive Esterel
distributed systems	Optimized Distributed Implementations of Timed Component-based Systems Design and Verification of Multi-Rate Distributed Systems
domain-specific language	On the Deployment Problem of Embedded Systems
E
embedded systems	On the Deployment Problem of Embedded Systems
Equivalency	Metric Interval Temporal Logic Specification Elicitation and Debugging
Esterel	SCEst: Sequentially Constructive Esterel
F
Fairness	Local and Global Fairness in Concurrent Systems
Formal modeling	Modeling and verifying context-aware non-monotonic reasoning agents
Formal Verification	Design and Verification of Multi-Rate Distributed Systems Towards Verification of Hybrid Systems in a Foundational Proof Assistant
foundational verification	Towards Verification of Hybrid Systems in a Foundational Proof Assistant
FPGA design emulation	From Signal Temporal Logic to FPGA Monitors
FSM extraction	Logic analysis and optimization with quick identification of invariants through one time frame analysis
H
Hardware	Implementing Latency-Insensitive Dataflow Blocks
Hardware description languages	A Generic Synthesisable Test Bench Layering RTL, SAFL, Handel-C and Bluespec Constructs on Chisel HCL
High-Assurance	Design and Verification of Multi-Rate Distributed Systems
high-level synthesis	C-To-Verilog Translation Validation
hybrid systems	Verification Condition Generation for Hybrid Systems Towards Verification of Hybrid Systems in a Foundational Proof Assistant From Non-Zenoness Verification to Termination
I
Induction	Logic analysis and optimization with quick identification of invariants through one time frame analysis
Invariant	Logic analysis and optimization with quick identification of invariants through one time frame analysis
K
Kahn networks	Implementing Latency-Insensitive Dataflow Blocks
L
latency-insensitive design	Implementing Latency-Insensitive Dataflow Blocks
Logic optimization with external don't care	Logic analysis and optimization with quick identification of invariants through one time frame analysis
Loop	Symbolic Loop Parallelization for Balancing I/O and Memory Accesses on Processor Arrays
M
machine learning	Passive testing of production systems based on model inference
medical software	Formal validation and verification of a medical software critical component
Memory subsystem verification	A Generic Synthesisable Test Bench
Metric Interval Temporal Logic	Metric Interval Temporal Logic Specification Elicitation and Debugging
model checking	Hierarchical Multi-Formalism Proofs of Cyber Physical Systems Model and Program Repair via SAT Solving Modeling and verifying context-aware non-monotonic reasoning agents
model inference	Passive testing of production systems based on model inference
Model repair	Model and Program Repair via SAT Solving
model transformations	Optimized Distributed Implementations of Timed Component-based Systems
Model-based development	Hierarchical Multi-Formalism Proofs of Cyber Physical Systems
Modeling	Modeling Resource Sharing using FSM-SADF
Multi-agent systems	Modeling and verifying context-aware non-monotonic reasoning agents
Multi-Rate Systems	Design and Verification of Multi-Rate Distributed Systems
N
nuXmv	Process algebra semantics and reachability analysis for micro-architectural models of communication fabrics
O
online monitoring	From Signal Temporal Logic to FPGA Monitors
optimization	On the Deployment Problem of Embedded Systems
P
parallelization	Symbolic Loop Parallelization for Balancing I/O and Memory Accesses on Processor Arrays
passive testing	Passive testing of production systems based on model inference
power reduction	Reducing power with activity trigger analysis
production system	Passive testing of production systems based on model inference
Program analysis and verification	Towards Refinement Types for Time-Dependent Data-Flow Networks
Programming language design	Towards Refinement Types for Time-Dependent Data-Flow Networks
proof assistants	Towards Verification of Hybrid Systems in a Foundational Proof Assistant
Property-based testing	A Generic Synthesisable Test Bench
Q
quadcopters	Towards Verification of Hybrid Systems in a Foundational Proof Assistant
quantified Boolean formula	Logic analysis and optimization with quick identification of invariants through one time frame analysis
R
reachability	Process algebra semantics and reachability analysis for micro-architectural models of communication fabrics
Real-time Systems	Optimized Distributed Implementations of Timed Component-based Systems Design and Verification of Multi-Rate Distributed Systems
Redundancy	Metric Interval Temporal Logic Specification Elicitation and Debugging
Resource Binding	Modeling Resource Sharing using FSM-SADF
Resource Sharing	Modeling Resource Sharing using FSM-SADF
RTL	Reducing power with activity trigger analysis
Rule-based reasoning	Modeling and verifying context-aware non-monotonic reasoning agents
runtime verification	From Signal Temporal Logic to FPGA Monitors Automatic and Configurable Instrumentation of C Programs with Temporal Assertion Checkers
S
SAFL	Layering RTL, SAFL, Handel-C and Bluespec Constructs on Chisel HCL
SAT solving	Model and Program Repair via SAT Solving
Satisfiability	Metric Interval Temporal Logic Specification Elicitation and Debugging
SCC-Invariants	Verification Condition Generation for Hybrid Systems
SCCharts	SCEst: Sequentially Constructive Esterel
Scenario-Aware Dataflow	Modeling Resource Sharing using FSM-SADF
SCEst	SCEst: Sequentially Constructive Esterel
Sequential Constructiveness	SCEst: Sequentially Constructive Esterel
signal temporal logic	Metric Interval Temporal Logic Specification Elicitation and Debugging From Signal Temporal Logic to FPGA Monitors
Software instrumentation	Automatic and Configurable Instrumentation of C Programs with Temporal Assertion Checkers
Stream-processing languages	Towards Refinement Types for Time-Dependent Data-Flow Networks
STS	Passive testing of production systems based on model inference
Synchronous Programming	SCEst: Sequentially Constructive Esterel
T
TCPAs	Symbolic Loop Parallelization for Balancing I/O and Memory Accesses on Processor Arrays
temporal logic	Towards Verification of Hybrid Systems in a Foundational Proof Assistant
Temporal properties	Automatic and Configurable Instrumentation of C Programs with Temporal Assertion Checkers
termination	From Non-Zenoness Verification to Termination
Test bench development	A Generic Synthesisable Test Bench
Tiling	Symbolic Loop Parallelization for Balancing I/O and Memory Accesses on Processor Arrays
Translation	Hierarchical Multi-Formalism Proofs of Cyber Physical Systems
translation validation	C-To-Verilog Translation Validation
Type theory	Towards Refinement Types for Time-Dependent Data-Flow Networks
V
Vacuity	Metric Interval Temporal Logic Specification Elicitation and Debugging
Verification	Local and Global Fairness in Concurrent Systems Hierarchical Multi-Formalism Proofs of Cyber Physical Systems C-To-Verilog Translation Validation
Verification & Validation	Formal validation and verification of a medical software critical component
Verification Condition Generation	Verification Condition Generation for Hybrid Systems
X
xMAS	Process algebra semantics and reachability analysis for micro-architectural models of communication fabrics
Z
zenoness	From Non-Zenoness Verification to Termination

Disclaimer | Powered by EasyChair Smart Program