FLOC 2018: FEDERATED LOGIC CONFERENCE 2018

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

Disclaimer | Powered by EasyChair Smart Program