FLOC 2018: FEDERATED LOGIC CONFERENCE 2018

A
Abstraction	Reasoning About TSO Programs Using Reduction and Abstraction (PDF, talk)
Abstraction Refinement	Space-time Interpolants (PDF, talk)
AI Safety	Safety-Aware Apprenticeship Learning (PDF, talk)
algorithm	Attracting Tangles to Solve Parity Games (PDF, talk)
Almost-sure winning	Symbolic Algorithms for Graphs and Markov Decision Processes with Fairness Objectives (PDF, talk)
AMBA AHB	Strix: Explicit Reactive Synthesis Strikes Back! (PDF, talk)
Android back stack	Android Stack Machine (PDF, talk)
Android stack systems	Android Stack Machine (PDF, talk)
Apprenticeship Learning	Safety-Aware Apprenticeship Learning (PDF, talk)
approximate circuits	ADAC: Automated Design of Approximate Circuits (PDF, talk)
approximate equivalence checking	ADAC: Automated Design of Approximate Circuits (PDF, talk)
Approximate synthesis	What’s hard about Boolean Functional Synthesis? (PDF, talk)
ASN.1	Formal Verification of a Vehicle-to-Vehicle (V2V) Messaging System (PDF, talk)
Asynchronous	Synthesis Of Asynchronous Reactive Programs From Temporal Specifications (PDF, talk)
automata	The Learnability of Symbolic Automata (PDF, talk)
automata learning	The Learnability of Symbolic Automata (PDF, talk)
automated reasoning	Understanding and Extending Incremental Determinization for 2QBF (PDF, talk) Model Generation for Quantified Formulas: A Taint-Based Approach (PDF, talk)
Automated verification	Constraint-Based Synthesis of Coupling Proofs (PDF, talk) Formal Verification of a Vehicle-to-Vehicle (V2V) Messaging System (PDF, talk)
Automatic Verification	The DEEPSEC prover (PDF, talk)
B
Barrier Certificates	Reachable Set Over-approximation for Nonlinear Systems Using Piecewise Barrier Tubes (PDF, talk)
Behavioural equivalence	The DEEPSEC prover (PDF, talk)
Bit-vectors	BTOR2, BtorMC and Boolector 3.0 (PDF, talk)
Boolean Functional synthesis	What’s hard about Boolean Functional Synthesis? (PDF, talk)
Boot code	Model Checking Boot Code from AWS Data Centers (PDF, talk)
bounded model checking	JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode (PDF, talk) Lazy Self-Composition for Security Verification (PDF, talk)
bounded synthesis	Synthesizing Reactive Systems from Hyperproperties (PDF, talk)
Bug Finding	Partial Order Aware Concurrency Sampling (PDF, talk)
bug finding tool	SimpleCAR: An Efficient Bug-Finding Tool Based On Approximate Reachability (PDF, talk)
C
cache coherence protocols	Eager Abstraction for Symbolic Model Checking (PDF, talk)
Cartesian Genetic Programming	ADAC: Automated Design of Approximate Circuits (PDF, talk)
CEGIS	Counterexample Guided Inductive Synthesis Modulo Theories (PDF, talk)
Comparator	Automata vs Linear-Programming Discounted-Sum Inclusion (PDF, talk)
complementary approximate reachability	SimpleCAR: An Efficient Bug-Finding Tool Based On Approximate Reachability (PDF, talk)
Computability	Program Analysis is Harder than Verification: A Computability Perspective (PDF, talk)
Computational Hardness	What’s hard about Boolean Functional Synthesis? (PDF, talk)
Concurrency Testing	Partial Order Aware Concurrency Sampling (PDF, talk)
Conditional Independence	Constrained Dynamic Partial Order Reduction (PDF, talk)
Conflict-Driven Clause Learning	The Proof Complexity of SMT Solvers (PDF, talk)
consistency	Monitoring Weak Consistency (PDF, talk)
Constraint-based synthesis	Constraint-Based Synthesis of Coupling Proofs (PDF, talk)
Constraint-based verification	Constraint-Based Synthesis of Coupling Proofs (PDF, talk)
Continuous-time Markov chain	Monitoring CTMCs By Multi-Clock Timed Automata (PDF, talk)
control improvisation	Reactive Control Improvisation (PDF, talk)
controller synthesis	Controller Synthesis Made Real: Reach-avoid Specifications and Linear Dynamics (PDF, talk)
conversion algorithm	A Direct Encoding for NNC Polyhedra (PDF, talk)
convex polyhedra	A Direct Encoding for NNC Polyhedra (PDF, talk)
Counterexample-Guided Inductive Synthesis	Safety-Aware Apprenticeship Learning (PDF, talk)
Cryptographic protocol	The DEEPSEC prover (PDF, talk)
Cryptographic software	SCInfer: Refinement-based Verification of Software Countermeasures against Side-Channel Attacks (PDF, talk)
Cryptography	Continuous formal verification of Amazon s2n (PDF, talk)
D
decision procedure	Android Stack Machine (PDF, talk)
decoupled approach	Controller Synthesis Made Real: Reach-avoid Specifications and Linear Dynamics (PDF, talk)
deductive verification	Eager Abstraction for Symbolic Model Checking (PDF, talk)
delay differential equations	Inner and Outer Approximating Flowpipes for Delay Differential Equations (PDF, talk)
Delta-completeness	Delta-Decision Procedures for Exists-Forall Problems over the Reals (PDF, talk)
Dependent Refinement Types	Propositional Dynamic Logic for Higher-Order Functional Programs (PDF, talk)
design automation	ADAC: Automated Design of Approximate Circuits (PDF, talk)
Deterministic Automata	Rabinizer 4: From LTL to Your Favourite Deterministic Automaton (PDF, talk)
Deterministic Parity Automaton	Strix: Explicit Reactive Synthesis Strikes Back! (PDF, talk)
Discounted-sum determinization	Automata vs Linear-Programming Discounted-Sum Inclusion (PDF, talk)
Discounted-sum inclusion	Automata vs Linear-Programming Discounted-Sum Inclusion (PDF, talk)
discrete-time linear system	Controller Synthesis Made Real: Reach-avoid Specifications and Linear Dynamics (PDF, talk)
distribute consensus protocols	Eager Abstraction for Symbolic Model Checking (PDF, talk)
distributed computing	Peregrine: A Tool for the Analysis of Population Protocols (PDF, talk)
Dolev-Yao Attacker	Model checking indistinguishability of randomized security protocols (PDF, talk)
Double Description method	A Direct Encoding for NNC Polyhedra (PDF, talk)
Dynamic analysis	Quasi-Optimal Partial Order Reduction (PDF, talk)
Dynamic data structures	Let this Graph be your Witness! An Attestor for Verifying Java Pointer Programs (PDF, talk)
Dynamic language	Nagini: A Static Verifier for Python (PDF, talk)
Dynamic Languages	MaxSMT-Based Type Inference for Python 3 (PDF, talk)
Dynamic Partial Order Reduction	Constrained Dynamic Partial Order Reduction (PDF, talk)
E
Electronic Voting	Model checking indistinguishability of randomized security protocols (PDF, talk)
Empirical evaluation	Automata vs Linear-Programming Discounted-Sum Inclusion (PDF, talk)
energy-efficient computing	ADAC: Automated Design of Approximate Circuits (PDF, talk)
F
Fairness objectives	Symbolic Algorithms for Graphs and Markov Decision Processes with Fairness Objectives (PDF, talk)
Firmware	Model Checking Boot Code from AWS Data Centers (PDF, talk)
first-order logic	Model Generation for Quantified Formulas: A Taint-Based Approach (PDF, talk)
formal languages and automata theory	Reactive Control Improvisation (PDF, talk)
Formal Methods	JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode (PDF, talk) The DEEPSEC prover (PDF, talk)
fuzzer	StringFuzz: A Fuzzer for String Solvers (PDF, talk)
G
graph grammars	Let this Graph be your Witness! An Attestor for Verifying Java Pointer Programs (PDF, talk)
H
Hardware/software interfaces	Model Checking Boot Code from AWS Data Centers (PDF, talk)
higher-order programs	Propositional Dynamic Logic for Higher-Order Functional Programs (PDF, talk)
Horn clauses	Constraint-Based Synthesis of Coupling Proofs (PDF, talk)
Hybrid System	Space-time Interpolants (PDF, talk)
Hyperproperties	Model Checking Quantitative Hyperproperties (PDF, talk) Synthesizing Reactive Systems from Hyperproperties (PDF, talk)
Hyperproperty Verification	Exploiting Synchrony and Symmetry in Relational Verification (PDF, talk)
I
Indistinguishability	Model checking indistinguishability of randomized security protocols (PDF, talk)
Inductive invariants	Syntax-Guided Termination Analysis (PDF, talk)
inductive validity cores	The JKind Model Checker (PDF, talk)
infinite-state systems	Eager Abstraction for Symbolic Model Checking (PDF, talk)
information flow analysis	Lazy Self-Composition for Security Verification (PDF, talk)
inner-approximations	Inner and Outer Approximating Flowpipes for Delay Differential Equations (PDF, talk)
integration	Continuous formal verification of Amazon s2n (PDF, talk)
Interpolation	Learning Abstractions for Program Synthesis (PDF, talk) Space-time Interpolants (PDF, talk)
Invariant Generation	Exploiting Synchrony and Symmetry in Relational Verification (PDF, talk)
Inverse Reinforcement Learning	Safety-Aware Apprenticeship Learning (PDF, talk)
J
Java	JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode (PDF, talk)
K
k-safety verification	Lazy Self-Composition for Security Verification (PDF, talk)
L
labelled Markov chain	Deciding Probabilistic Bisimilarity Distance One for Labelled Markov Chains (PDF, talk)
Language inclusion	Automata vs Linear-Programming Discounted-Sum Inclusion (PDF, talk)
lazy self-composition	Lazy Self-Composition for Security Verification (PDF, talk)
learning	The Learnability of Symbolic Automata (PDF, talk)
Linear Temporal Logic	Rabinizer 4: From LTL to Your Favourite Deterministic Automaton (PDF, talk) Strix: Explicit Reactive Synthesis Strikes Back! (PDF, talk)
linearizability	Monitoring Weak Consistency (PDF, talk)
Liveness Analysis	Symbolic Liveness Analysis of Real-World Software (PDF, talk)
LLVM	Formal Verification of a Vehicle-to-Vehicle (V2V) Messaging System (PDF, talk)
Logic Solvers	Understanding and Extending Incremental Determinization for 2QBF (PDF, talk)
M
Machine Learning	Fast Numerical Program Analysis with Reinforcement Learning (PDF, talk)
Markov decision processes	Value Iteration for Simple Stochastic Games: Stopping Criterion and Learning Algorithm (PDF, talk) Sound Value Iteration (PDF, talk) Symbolic Algorithms for Graphs and Markov Decision Processes with Fairness Objectives (PDF, talk)
message passing concurrency	On the Completeness of Verifying Message Passing Programs under Bounded Asynchrony (PDF, talk)
model checking	Propositional Dynamic Logic for Higher-Order Functional Programs (PDF, talk) Model Checking Quantitative Hyperproperties (PDF, talk) Eager Abstraction for Symbolic Model Checking (PDF, talk) Monitoring CTMCs By Multi-Clock Timed Automata (PDF, talk) Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems (PDF, talk) BTOR2, BtorMC and Boolector 3.0 (PDF, talk) The JKind Model Checker (PDF, talk) SimpleCAR: An Efficient Bug-Finding Tool Based On Approximate Reachability (PDF, talk) Attracting Tangles to Solve Parity Games (PDF, talk) On the Completeness of Verifying Message Passing Programs under Bounded Asynchrony (PDF, talk) Constrained Dynamic Partial Order Reduction (PDF, talk) Model Checking Boot Code from AWS Data Centers (PDF, talk)
Model Counting	Model Checking Quantitative Hyperproperties (PDF, talk)
model generation	Model Generation for Quantified Formulas: A Taint-Based Approach (PDF, talk)
Modular Arithmetic	Formally Verified Montgomery Multiplication (PDF, talk)
Montgomery Multiplication	Formally Verified Montgomery Multiplication (PDF, talk)
Multi-clock timed automata	Monitoring CTMCs By Multi-Clock Timed Automata (PDF, talk)
N
Non-interleaving semantics	Quasi-Optimal Partial Order Reduction (PDF, talk)
Non-Termination Bugs	Symbolic Liveness Analysis of Real-World Software (PDF, talk)
Non-termination Proving	Syntax-Guided Termination Analysis (PDF, talk)
Numerical Program Analysis	Fast Numerical Program Analysis with Reinforcement Learning (PDF, talk)
O
Online Decomposition	Fast Numerical Program Analysis with Reinforcement Learning (PDF, talk)
optimization	Delta-Decision Procedures for Exists-Forall Problems over the Reals (PDF, talk)
Ordinary differential equation	Monitoring CTMCs By Multi-Clock Timed Automata (PDF, talk)
P
parameterized systems	Eager Abstraction for Symbolic Model Checking (PDF, talk)
parameterized verification	Peregrine: A Tool for the Analysis of Population Protocols (PDF, talk)
Parity Game	Strix: Explicit Reactive Synthesis Strikes Back! (PDF, talk) Attracting Tangles to Solve Parity Games (PDF, talk)
partial order reduction	Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems (PDF, talk) Partial Order Aware Concurrency Sampling (PDF, talk)
Partial-order reduction	Quasi-Optimal Partial Order Reduction (PDF, talk)
Perfect masking	SCInfer: Refinement-based Verification of Software Countermeasures against Side-Channel Attacks (PDF, talk)
permission inference	Permission Inference for Array Programs (PDF, talk)
Polyhedra Domain Analysis	Fast Numerical Program Analysis with Reinforcement Learning (PDF, talk)
population protocols	Peregrine: A Tool for the Analysis of Population Protocols (PDF, talk)
Privacy-type properties	The DEEPSEC prover (PDF, talk)
probabilistic bisimilarity	Deciding Probabilistic Bisimilarity Distance One for Labelled Markov Chains (PDF, talk)
probabilistic bisimilarity distance	Deciding Probabilistic Bisimilarity Distance One for Labelled Markov Chains (PDF, talk)
Probabilistic Boolean Program	SCInfer: Refinement-based Verification of Software Countermeasures against Side-Channel Attacks (PDF, talk)
probabilistic games	Reactive Control Improvisation (PDF, talk)
Probabilistic model checking	Sound Value Iteration (PDF, talk) Safety-Aware Apprenticeship Learning (PDF, talk)
Probabilistic programs	Constraint-Based Synthesis of Coupling Proofs (PDF, talk)
Probabilistic State Space Exploration	Partial Order Aware Concurrency Sampling (PDF, talk)
probabilistic verification	Constraint-Based Synthesis of Coupling Proofs (PDF, talk) Value Iteration for Simple Stochastic Games: Stopping Criterion and Learning Algorithm (PDF, talk)
Program Analysis	Quasi-Optimal Partial Order Reduction (PDF, talk)
Program Synthesis	Syntax-Guided Termination Analysis (PDF, talk) Counterexample Guided Inductive Synthesis Modulo Theories (PDF, talk) Constraint-Based Synthesis of Coupling Proofs (PDF, talk) Syntax Guided Synthesis with Quantitative Syntactic Objectives (PDF, talk) Learning Abstractions for Program Synthesis (PDF, talk)
Program Verification	Syntax-Guided Termination Analysis (PDF, talk) Nagini: A Static Verifier for Python (PDF, talk) Program Analysis is Harder than Verification: A Computability Perspective (PDF, talk) Formally Verified Montgomery Multiplication (PDF, talk)
Programming-by-Example	Learning Abstractions for Program Synthesis (PDF, talk)
Proof	Continuous formal verification of Amazon s2n (PDF, talk)
proof complexity	The Proof Complexity of SMT Solvers (PDF, talk)
property falsification	Inner and Outer Approximating Flowpipes for Delay Differential Equations (PDF, talk)
Propositional Dynamic Logic	Propositional Dynamic Logic for Higher-Order Functional Programs (PDF, talk)
Protocol Verification	Model checking indistinguishability of randomized security protocols (PDF, talk)
Pushdown systems with transductions	Android Stack Machine (PDF, talk)
Q
QBF	Synthesis Of Asynchronous Reactive Programs From Temporal Specifications (PDF, talk)
Quantified Bit-Vectors	Solving Quantified Bit-Vectors using Invertibility Conditions (PDF, talk)
Quantified Boolean Formulas	Understanding and Extending Incremental Determinization for 2QBF (PDF, talk)
Quantifier	Delta-Decision Procedures for Exists-Forall Problems over the Reals (PDF, talk)
Quantitative Analysis	Automata vs Linear-Programming Discounted-Sum Inclusion (PDF, talk)
Quantitative Objective	Syntax Guided Synthesis with Quantitative Syntactic Objectives (PDF, talk)
Quantitative Semantics for Temporal Logic	A Counting Semantics for Monitoring LTL Specifications over Finite Traces (PDF, talk)
R
Randomization	Model checking indistinguishability of randomized security protocols (PDF, talk)
Randomized algorithms	Constraint-Based Synthesis of Coupling Proofs (PDF, talk)
reach-avoid specification	Controller Synthesis Made Real: Reach-avoid Specifications and Linear Dynamics (PDF, talk)
reachability	Value Iteration for Simple Stochastic Games: Stopping Criterion and Learning Algorithm (PDF, talk)
reachability analysis	SimpleCAR: An Efficient Bug-Finding Tool Based On Approximate Reachability (PDF, talk) Inner and Outer Approximating Flowpipes for Delay Differential Equations (PDF, talk)
Reachability analysis of nonlinear systems	Reachable Set Over-approximation for Nonlinear Systems Using Piecewise Barrier Tubes (PDF, talk)
Reachability problem	Android Stack Machine (PDF, talk)
Reachable set over-approximation	Reachable Set Over-approximation for Nonlinear Systems Using Piecewise Barrier Tubes (PDF, talk)
reactive synthesis	Reactive Control Improvisation (PDF, talk) Strix: Explicit Reactive Synthesis Strikes Back! (PDF, talk)
Realizability	Synthesizing Reactive Systems from Hyperproperties (PDF, talk)
Reduction	Reasoning About TSO Programs Using Reduction and Abstraction (PDF, talk)
Reinforcement Learning	Fast Numerical Program Analysis with Reinforcement Learning (PDF, talk) Safety-Aware Apprenticeship Learning (PDF, talk)
Relational Verification	Exploiting Synchrony and Symmetry in Relational Verification (PDF, talk)
Resolution	The Proof Complexity of SMT Solvers (PDF, talk)
Rice's theorem	Program Analysis is Harder than Verification: A Computability Perspective (PDF, talk)
robotic planning	Reactive Control Improvisation (PDF, talk)
robustness	Reasoning About TSO Programs Using Reduction and Abstraction (PDF, talk) Inner and Outer Approximating Flowpipes for Delay Differential Equations (PDF, talk)
Runtime complexity	Automata vs Linear-Programming Discounted-Sum Inclusion (PDF, talk)
runtime verification	Monitoring Weak Consistency (PDF, talk) A Counting Semantics for Monitoring LTL Specifications over Finite Traces (PDF, talk)
S
SAT	Understanding and Extending Incremental Determinization for 2QBF (PDF, talk)
SAT and BDD-based decision procedures	ADAC: Automated Design of Approximate Circuits (PDF, talk)
SAT modulo theories	Eager Abstraction for Symbolic Model Checking (PDF, talk)
Satisfiability Modulo Theories	Solving Quantified Bit-Vectors using Invertibility Conditions (PDF, talk) The Proof Complexity of SMT Solvers (PDF, talk)
Security	The DEEPSEC prover (PDF, talk) Formal Verification of a Vehicle-to-Vehicle (V2V) Messaging System (PDF, talk)
security verification	Lazy Self-Composition for Security Verification (PDF, talk)
self-composition	Lazy Self-Composition for Security Verification (PDF, talk)
separation logic	Nagini: A Static Verifier for Python (PDF, talk) Permission Inference for Array Programs (PDF, talk)
Side-channel attack	SCInfer: Refinement-based Verification of Software Countermeasures against Side-Channel Attacks (PDF, talk)
simulation	Peregrine: A Tool for the Analysis of Population Protocols (PDF, talk)
Skolem functions	What’s hard about Boolean Functional Synthesis? (PDF, talk)
SMT	Constraint-Based Synthesis of Coupling Proofs (PDF, talk) StringFuzz: A Fuzzer for String Solvers (PDF, talk) Delta-Decision Procedures for Exists-Forall Problems over the Reals (PDF, talk) Constrained Dynamic Partial Order Reduction (PDF, talk)
SMT Solver	Formal Verification of a Vehicle-to-Vehicle (V2V) Messaging System (PDF, talk)
SMT solvers	Controller Synthesis Made Real: Reach-avoid Specifications and Linear Dynamics (PDF, talk) The Proof Complexity of SMT Solvers (PDF, talk)
SMT Solving	BTOR2, BtorMC and Boolector 3.0 (PDF, talk) MaxSMT-Based Type Inference for Python 3 (PDF, talk) Solving Quantified Bit-Vectors using Invertibility Conditions (PDF, talk)
Software model checking	Let this Graph be your Witness! An Attestor for Verifying Java Pointer Programs (PDF, talk)
Software Testing	Symbolic Liveness Analysis of Real-World Software (PDF, talk)
software verification	JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode (PDF, talk) On the Completeness of Verifying Message Passing Programs under Bounded Asynchrony (PDF, talk)
Specification-based monitoring	A Counting Semantics for Monitoring LTL Specifications over Finite Traces (PDF, talk)
Stack-Based Access Control	Propositional Dynamic Logic for Higher-Order Functional Programs (PDF, talk)
State-space abstraction	Let this Graph be your Witness! An Attestor for Verifying Java Pointer Programs (PDF, talk)
Static Analysis	Fast Numerical Program Analysis with Reinforcement Learning (PDF, talk) Permission Inference for Array Programs (PDF, talk) Constrained Dynamic Partial Order Reduction (PDF, talk)
Static program analysis	Program Analysis is Harder than Verification: A Computability Perspective (PDF, talk)
stochastic games	Value Iteration for Simple Stochastic Games: Stopping Criterion and Learning Algorithm (PDF, talk)
Streett objectives	Symbolic Algorithms for Graphs and Markov Decision Processes with Fairness Objectives (PDF, talk)
strict inequalities	A Direct Encoding for NNC Polyhedra (PDF, talk)
strings	StringFuzz: A Fuzzer for String Solvers (PDF, talk)
stubborn sets	Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems (PDF, talk)
SyGuS	Syntax Guided Synthesis with Quantitative Syntactic Objectives (PDF, talk)
Symbolic Algorithms	Symbolic Algorithms for Graphs and Markov Decision Processes with Fairness Objectives (PDF, talk)
symbolic automata	The Learnability of Symbolic Automata (PDF, talk)
Symbolic Execution	Formal Verification of a Vehicle-to-Vehicle (V2V) Messaging System (PDF, talk) Symbolic Liveness Analysis of Real-World Software (PDF, talk) Model Checking Boot Code from AWS Data Centers (PDF, talk)
Symbolic model	The DEEPSEC prover (PDF, talk)
Symmetry-Breaking Predicates	Exploiting Synchrony and Symmetry in Relational Verification (PDF, talk)
Syntax guided synthesis	Counterexample Guided Inductive Synthesis Modulo Theories (PDF, talk)
Synthesis	Synthesizing Reactive Systems from Hyperproperties (PDF, talk) Synthesis Of Asynchronous Reactive Programs From Temporal Specifications (PDF, talk) Rabinizer 4: From LTL to Your Favourite Deterministic Automaton (PDF, talk) Attracting Tangles to Solve Parity Games (PDF, talk) Understanding and Extending Incremental Determinization for 2QBF (PDF, talk)
Systematic Testing	Partial Order Aware Concurrency Sampling (PDF, talk)
T
taint analysis	Lazy Self-Composition for Security Verification (PDF, talk)
Taylor models	Inner and Outer Approximating Flowpipes for Delay Differential Equations (PDF, talk)
Temporal Logic	Synthesis Of Asynchronous Reactive Programs From Temporal Specifications (PDF, talk)
Temporal Verification	Propositional Dynamic Logic for Higher-Order Functional Programs (PDF, talk)
Termination Proving	Syntax-Guided Termination Analysis (PDF, talk)
test case generation	The JKind Model Checker (PDF, talk)
Theorem Proving by Induction	Formally Verified Montgomery Multiplication (PDF, talk)
timed systems	Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems (PDF, talk)
timed-arc Petri nets	Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems (PDF, talk)
Total Store Ordering	Reasoning About TSO Programs Using Reduction and Abstraction (PDF, talk)
traceability	The JKind Model Checker (PDF, talk)
Type Inference	MaxSMT-Based Type Inference for Python 3 (PDF, talk)
U
under-approximations	Inner and Outer Approximating Flowpipes for Delay Differential Equations (PDF, talk)
Uninterpreted Function Symbols	The Proof Complexity of SMT Solvers (PDF, talk)
V
value iteration	Value Iteration for Simple Stochastic Games: Stopping Criterion and Learning Algorithm (PDF, talk) Sound Value Iteration (PDF, talk)
Vehicle-to-Vehicle	Formal Verification of a Vehicle-to-Vehicle (V2V) Messaging System (PDF, talk)
Verification	Rabinizer 4: From LTL to Your Favourite Deterministic Automaton (PDF, talk) SCInfer: Refinement-based Verification of Software Countermeasures against Side-Channel Attacks (PDF, talk) Continuous formal verification of Amazon s2n (PDF, talk)

Disclaimer | Powered by EasyChair Smart Program