FLOC 2018: FEDERATED LOGIC CONFERENCE 2018

A
Abate, Alessandro	Synthesis Modulo Theories
Akshay, S.	What’s hard about Boolean Functional Synthesis?
Albarghouthi, Aws	Constraint-Based Synthesis of Coupling Proofs
Albert, Elvira	Constrained Dynamic Partial Order Reduction
Anderson, Greg	Learning Abstractions for Program Synthesis
Argyros, George	The Learnability of Symbolic Automata
Arndt, Hannah	Let this Graph be your Witness! An Attestor for Verifying Java Pointer Programs
B
Backes, John	The JKind Model Checker
Bansal, Suguman	Automata vs Linear-Programming Discounted-Sum Inclusion Synthesis Of Asynchronous Reactive Programs From Temporal Specifications
Bardin, Sebastien	Model Generation for Quantified Formulas: A Taint-Based Approach
Barrett, Clark	Solving Quantified Bit-Vectors using Invertibility Conditions
Bartocci, Ezio	Reachable Set Over-approximation for Nonlinear Systems Using Piecewise Barrier Tubes A Counting Semantics for Monitoring LTL Specifications over Finite Traces
Bauer, Matthew	Model checking indistinguishability of randomized security protocols
Becchi, Anna	A Direct Encoding for NNC Polyhedra
Berzish, Murphy	StringFuzz: A Fuzzer for String Solvers
Biere, Armin	BTOR2, BtorMC and Boolector 3.0
Bloem, Roderick	A Counting Semantics for Monitoring LTL Specifications over Finite Traces
Blondin, Michael	Peregrine: A Tool for the Analysis of Population Protocols
Blotsky, Dmitry	StringFuzz: A Fuzzer for String Solvers
Bonichon, Richard	Model Generation for Quantified Formulas: A Taint-Based Approach
Bouajjani, Ahmed	Reasoning About TSO Programs Using Reduction and Abstraction On the Completeness of Verifying Message Passing Programs under Bounded Asynchrony
Bønneland, Frederik M.	Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems
Büning, Julian	Symbolic Liveness Analysis of Real-World Software
C
Ceska, Milan	ADAC: Automated Design of Approximate Circuits
Chadha, Rohit	Model checking indistinguishability of randomized security protocols
Chakraborty, Supratik	What’s hard about Boolean Functional Synthesis?
Chatterjee, Krishnendu	Symbolic Algorithms for Graphs and Markov Decision Processes with Fairness Objectives
Chaudhuri, Swarat	Automata vs Linear-Programming Discounted-Sum Inclusion
Chen, Taolue	Android Stack Systems
Cheval, Vincent	The DEEPSEC prover
Chudnov, Andrey	Continuous formal verification of Amazon s2n
Collins, Nathan	Formal Verification of a Vehicle-to-Vehicle (V2V) Messaging System Continuous formal verification of Amazon s2n
Cook, Byron	Continuous formal verification of Amazon s2n Model Checking Boot Code from AWS Data Centers
Cordeiro, Lucas	JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode
Coti, Camille	Quasi-Optimal Partial Order Reduction
Cousot, Patrick	Program Analysis is Harder than Verification: A Computability Perspective
D
D'Antoni, Loris	The Learnability of Symbolic Automata Syntax Guided Synthesis with Quantitative Syntactic Objectives
David, Cristina	Synthesis Modulo Theories
Dillig, Isil	Learning Abstractions for Program Synthesis
Dodds, Josiah	Continuous formal verification of Amazon s2n
Dohrau, Jérôme	Permission Inference for Array Programs
Dureja, Rohit	SimpleCAR: An Efficient Bug-Finding Tool Based On Approximate Reachability
E
Eilers, Marco	MaxSMT-Based Type Inference for Python 3 Nagini: A Static Verifier for Python
Emmi, Michael	Monitoring Weak Consistency
Enea, Constantin	Monitoring Weak Consistency Reasoning About TSO Programs Using Reduction and Abstraction On the Completeness of Verifying Message Passing Programs under Bounded Asynchrony
Esparza, Javier	Peregrine: A Tool for the Analysis of Population Protocols
F
Fan, Chuchu	Controller Synthesis Made Real: Reach-avoid Specifications and Linear Dynamics
Farinier, Benjamin	Model Generation for Quantified Formulas: A Taint-Based Approach
Fedyukovich, Grigory	Syntax-Guided Termination Analysis Exploiting Synchrony and Symmetry in Relational Verification
Feng, Yijun	Monitoring CTMCs By Multi-Clock Timed Automata
Finkbeiner, Bernd	Model Checking Quantitative Hyperproperties Synthesizing Reactive Systems from Hyperproperties
Frehse, Goran	Spacetime Interpolants
Fremont, Daniel J.	Reactive Control Improvisation
G
Gacek, Andrew	The JKind Model Checker
Ganesh, Vijay	StringFuzz: A Fuzzer for String Solvers The Proof Complexity of SMT Solvers
Gao, Pengfei	SCInfer: Refinement-based Verification of Software Countermeasures against Side-Channel Attacks
Gao, Sicun	Delta-Decision Procedures for Exists-Forall Problems over the Reals
Ghassabani, Elaheh	The JKind Model Checker
Giacobazzi, Roberto	Program Analysis is Harder than Verification: A Computability Perspective
Giacobbe, Mirco	Spacetime Interpolants
Goel, Shubham	What’s hard about Boolean Functional Synthesis?
Gomez-Zamalloa, Miguel	Constrained Dynamic Partial Order Reduction
Goubault, Eric	Inner and Outer Approximating Flowpipes for Delay Differential Equations
Gu, Ronghui	Partial Order Aware Concurrency Sampling
Guldstrand Larsen, Kim	Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems
Gupta, Aarti	Lazy Self-Composition for Security Verification Syntax-Guided Termination Analysis Exploiting Synchrony and Symmetry in Relational Verification
H
Hahn, Christopher	Model Checking Quantitative Hyperproperties Synthesizing Reactive Systems from Hyperproperties
Hassan, Mostafa	MaxSMT-Based Type Inference for Python 3
He, Jinlong	Android Stack Systems
Henzinger, Monika	Symbolic Algorithms for Graphs and Markov Decision Processes with Fairness Objectives
Henzinger, Tom	Reachable Set Over-approximation for Nonlinear Systems Using Piecewise Barrier Tubes Spacetime Interpolants
Hsu, Justin	Constraint-Based Synthesis of Coupling Proofs
Hu, Qinheping	Syntax Guided Synthesis with Quantitative Syntactic Objectives
Huffman, Brian	Continuous formal verification of Amazon s2n
I
Isabel, Miguel	Constrained Dynamic Partial Order Reduction
J
Jaax, Stefan	Peregrine: A Tool for the Analysis of Population Protocols
Jansen, Christina	Let this Graph be your Witness! An Attestor for Verifying Java Pointer Programs
Jensen, Peter Gjøl	Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems
Jha, Somesh	Semantic Adversarial Deep Learning
Ji, Kailiang	On the Completeness of Verifying Message Passing Programs under Bounded Asynchrony
K
Kabir, Ifaz	StringFuzz: A Fuzzer for String Solvers
Katoen, Joost-Pieter	Let this Graph be your Witness! An Attestor for Verifying Java Pointer Programs Monitoring CTMCs By Multi-Clock Timed Automata Sound Value Iteration
Kelmendi, Edon	Value Iteration for Simple Stochastic Games: Stopping Criterion and Learning Algorithm
Kesseli, Pascal	JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode Synthesis Modulo Theories
Khazem, Kareem	Model Checking Boot Code from AWS Data Centers
Kolokolova, Antonina	The Proof Complexity of SMT Solvers
Kong, Hui	Reachable Set Over-approximation for Nonlinear Systems Using Piecewise Barrier Tubes
Kong, Soonho	Delta-Decision Procedures for Exists-Forall Problems over the Reals
Kragl, Bernhard	Proving a concurrent program correct by demonstrating it does nothing Proving a concurrent program correct by demonstrating it does nothing (continued)
Kremer, Steve	The DEEPSEC prover
Kretinsky, Jan	Rabinizer 4: From LTL to Your Favourite Deterministic Automaton Value Iteration for Simple Stochastic Games: Stopping Criterion and Learning Algorithm
Kroening, Daniel	JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode Synthesis Modulo Theories Model Checking Boot Code from AWS Data Centers
Krämer, Julia	Value Iteration for Simple Stochastic Games: Stopping Criterion and Learning Algorithm
Kulal, Sumith	What’s hard about Boolean Functional Synthesis?
L
Li, Haokun	Monitoring CTMCs By Multi-Clock Timed Automata
Li, Jianwen	SimpleCAR: An Efficient Bug-Finding Tool Based On Approximate Reachability
Li, Wenchao	Safety-Aware Apprenticeship Learning
Loitzenbauer, Veronika	Symbolic Algorithms for Graphs and Markov Decision Processes with Fairness Objectives
Lukert, Philip	Synthesizing Reactive Systems from Hyperproperties
Luttenberger, Michael	Strix: Explicit Reactive Synthesis Strikes Back!
M
MacCarthaigh, Colm	Continuous formal verification of Amazon s2n
Maffei, Matteo	Foundations and Techniques for the Static Analysis of Ethereum Smart Contracts
Magill, Stephen	Continuous formal verification of Amazon s2n
Malik, Sharad	Lazy Self-Composition for Security Verification
Matheja, Christoph	Let this Graph be your Witness! An Attestor for Verifying Java Pointer Programs
Mathur, Umang	Controller Synthesis Made Real: Reach-avoid Specifications and Linear Dynamics
Matyas, Jiri	ADAC: Automated Design of Approximate Circuits
McMillan, Ken	Learning Abstractions for Program Synthesis Eager Abstraction for Symbolic Model Checking
Meggendorfer, Tobias	Rabinizer 4: From LTL to Your Favourite Deterministic Automaton
Melham, Tom	Proof Scripting from HOL to Goaled
Mertens, Eric	Continuous formal verification of Amazon s2n
Meyer, Philipp J.	Strix: Explicit Reactive Synthesis Strikes Back!
Mitra, Sayan	Controller Synthesis Made Real: Reach-avoid Specifications and Linear Dynamics
Mora, Federico	StringFuzz: A Fuzzer for String Solvers
Mrazek, Vojtech	ADAC: Automated Design of Approximate Circuits
Mullen, Eric	Continuous formal verification of Amazon s2n
Mutluergil, Suha Orhun	Reasoning About TSO Programs Using Reduction and Abstraction
Muñiz, Marco	Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems
Myreen, Magnus	From Processor Verification Upwards
Müller, Peter	MaxSMT-Based Type Inference for Python 3 Permission Inference for Array Programs Nagini: A Static Verifier for Python
Münger, Severin	Permission Inference for Array Programs
N
Namjoshi, Kedar	Synthesis Of Asynchronous Reactive Programs From Temporal Specifications
Nguyen, Huyen T.T.	Quasi-Optimal Partial Order Reduction
Nickovic, Dejan	A Counting Semantics for Monitoring LTL Specifications over Finite Traces
Niemetz, Aina	Solving Quantified Bit-Vectors using Invertibility Conditions BTOR2, BtorMC and Boolector 3.0
Noll, Thomas	Let this Graph be your Witness! An Attestor for Verifying Java Pointer Programs Symbolic Liveness Analysis of Real-World Software
Norrish, Michael	HOL Developed and HOL Used: Interconnected Stories of Real-World Applications
O
Oraee, Simin	Symbolic Algorithms for Graphs and Markov Decision Processes with Fairness Objectives
P
Petrucci, Laure	Quasi-Optimal Partial Order Reduction
Pick, Lauren	Exploiting Synchrony and Symmetry in Relational Verification
Pike, Lee	Formal Verification of a Vehicle-to-Vehicle (V2V) Messaging System
Polgreen, Elizabeth	Synthesis Modulo Theories
Potet, Marie-Laure	Model Generation for Quantified Formulas: A Taint-Based Approach
Preiner, Mathias	Solving Quantified Bit-Vectors using Invertibility Conditions BTOR2, BtorMC and Boolector 3.0
Pu, Geguang	SimpleCAR: An Efficient Bug-Finding Tool Based On Approximate Reachability
Putot, Sylvie	Inner and Outer Approximating Flowpipes for Delay Differential Equations
Püschel, Markus	Fast Numerical Program Analysis with Reinforcement Learning
Q
Qadeer, Shaz	Proving a concurrent program correct by demonstrating it does nothing Proving a concurrent program correct by demonstrating it does nothing (continued) On the Completeness of Verifying Message Passing Programs under Bounded Asynchrony
Quatmann, Tim	Sound Value Iteration
R
Rabe, Markus N.	Understanding and Extending Incremental Determinization for 2QBF
Rakotonirina, Itsaka	The DEEPSEC prover
Ranzato, Francesco	Program Analysis is Harder than Verification: A Computability Perspective
Rasmussen, Cameron	Understanding and Extending Incremental Determinization for 2QBF
Reynolds, Andrew	Solving Quantified Bit-Vectors using Invertibility Conditions
Robere, Robert	The Proof Complexity of SMT Solvers
Rodriguez, Cesar	Quasi-Optimal Partial Order Reduction
Roeck, Franz	A Counting Semantics for Monitoring LTL Specifications over Finite Traces
Rozier, Kristin Yvonne	SimpleCAR: An Efficient Bug-Finding Tool Based On Approximate Reachability
Rubio, Albert	Constrained Dynamic Partial Order Reduction
S
Sa'Ar, Yaniv	Synthesis Of Asynchronous Reactive Programs From Temporal Specifications
Sahlman, Lorenz	Inner and Outer Approximating Flowpipes for Delay Differential Equations
Satake, Yuki	Propositional Dynamic Logic for Higher-Order Functional Programs
Schemmel, Daniel	Symbolic Liveness Analysis of Real-World Software
Schneidewind, Clara	Foundations and Techniques for the Static Analysis of Ethereum Smart Contracts
Schrammel, Peter	JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode
Sekanina, Lukas	ADAC: Automated Design of Approximate Circuits
Seshia, Sanjit A.	Understanding and Extending Incremental Determinization for 2QBF Reactive Control Improvisation
Shah, Shetal	What’s hard about Boolean Functional Synthesis?
Sickert, Salomon	Rabinizer 4: From LTL to Your Favourite Deterministic Automaton Strix: Explicit Reactive Synthesis Strikes Back!
Singh, Gagandeep	Fast Numerical Program Analysis with Reinforcement Learning
Sistla, Prasad	Model checking indistinguishability of randomized security protocols
Solar-Lezama, Armando	Delta-Decision Procedures for Exists-Forall Problems over the Reals
Song, Fu	SCInfer: Refinement-based Verification of Software Countermeasures against Side-Channel Attacks Android Stack Systems
Soria Dustmann, Oscar	Symbolic Liveness Analysis of Real-World Software
Sousa, Marcelo	Quasi-Optimal Partial Order Reduction
Srba, Jiri	Start Pruning When Time Gets Urgent: Partial Order Reduction for Timed Systems
Stenger, Marvin	Synthesizing Reactive Systems from Hyperproperties
Subramanyan, Pramod	Lazy Self-Composition for Security Verification
Summers, Alexander J	Permission Inference for Array Programs
T
Tang, Qiyi	Deciding Probabilistic Bisimilarity Distance One for Labelled Markov Chains
Tasiran, Serdar	Reasoning About TSO Programs Using Reduction and Abstraction Continuous formal verification of Amazon s2n Model Checking Boot Code from AWS Data Centers
Tautschnig, Michael	Model Checking Boot Code from AWS Data Centers
Tentrup, Leander	Understanding and Extending Incremental Determinization for 2QBF Synthesizing Reactive Systems from Hyperproperties
Tinelli, Cesare	Solving Quantified Bit-Vectors using Invertibility Conditions
Toman, Viktor	Symbolic Algorithms for Graphs and Markov Decision Processes with Fairness Objectives
Tomb, Aaron	Formal Verification of a Vehicle-to-Vehicle (V2V) Messaging System Continuous formal verification of Amazon s2n
Torfah, Hazem	Model Checking Quantitative Hyperproperties
Trtik, Marek	JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode
Tullsen, Mark	Formal Verification of a Vehicle-to-Vehicle (V2V) Messaging System
Tuttle, Mark R.	Model Checking Boot Code from AWS Data Centers
U
Unno, Hiroshi	Propositional Dynamic Logic for Higher-Order Functional Programs
Urban, Caterina	MaxSMT-Based Type Inference for Python 3 Permission Inference for Array Programs
V
van Breugel, Franck	Deciding Probabilistic Bisimilarity Distance One for Labelled Markov Chains
van Dijk, Tom	Attracting Tangles to Solve Parity Games
Vardi, Moshe	Automata vs Linear-Programming Discounted-Sum Inclusion
Vardi, Moshe	SimpleCAR: An Efficient Bug-Finding Tool Based On Approximate Reachability
Vasicek, Zdenek	ADAC: Automated Design of Approximate Circuits
Vechev, Martin	Fast Numerical Program Analysis with Reinforcement Learning
Viswanathan, Mahesh	Model checking indistinguishability of randomized security protocols Controller Synthesis Made Real: Reach-avoid Specifications and Linear Dynamics
Vizel, Yakir	Lazy Self-Composition for Security Verification
Vojnar, Tomas	ADAC: Automated Design of Approximate Circuits
W
Wagner, Lucas	The JKind Model Checker
Walther, Christoph	Formally Verified Montgomery Multiplication
Wang, Chao	SCInfer: Refinement-based Verification of Software Countermeasures against Side-Channel Attacks
Wang, Guozhen	Android Stack Systems
Wang, Xinyu	Learning Abstractions for Program Synthesis
Wehrle, Klaus	Symbolic Liveness Analysis of Real-World Software
Weininger, Maximilian	Value Iteration for Simple Stochastic Games: Stopping Criterion and Learning Algorithm
Westbrook, Edwin	Continuous formal verification of Amazon s2n
Whalen, Michael	The JKind Model Checker
Wolf, Clifford	BTOR2, BtorMC and Boolector 3.0
Wu, Zhilin	Android Stack Systems
X
Xia, Bican	Monitoring CTMCs By Multi-Clock Timed Automata
Y
Yahav, Eran	From Programs to interpretable Deep Models, and Back
Yan, Jun	Android Stack Systems
Yang, Junfeng	Partial Order Aware Concurrency Sampling
Yang, Weikun	Lazy Self-Composition for Security Verification
Yuan, Xinhao	Partial Order Aware Concurrency Sampling
Z
Zaffanella, Enea	A Direct Encoding for NNC Polyhedra
Zhan, Naijun	Monitoring CTMCs By Multi-Clock Timed Automata
Zhang, Jun	SCInfer: Refinement-based Verification of Software Countermeasures against Side-Channel Attacks
Zhang, Yueling	Syntax-Guided Termination Analysis
Zheng, Yunhui	StringFuzz: A Fuzzer for String Solvers
Zhou, Weichao	Safety-Aware Apprenticeship Learning

Disclaimer | Powered by EasyChair Smart Program