FLOC 2018: FEDERATED LOGIC CONFERENCE 2018

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

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

Disclaimer | Powered by EasyChair Smart Program