FMCAD 2018: FORMAL METHODS IN COMPUTER AIDED DESIGN 2018

A
Abdulla, Parosh Aziz	Trau: SMT solver for string constraints
Aichernig, Bernhard K.	Automata Learning for Symbolic Execution
Anand, Sourav	Automatic Synchronization for GPU Kernels
Atig, Mohamed Faouzi	Trau: SMT solver for string constraints
B
Backeman, Peter	Bit-Vector Interpolation and Quantifier Elimination by Lazy Reduction
Backes, John	Semantic-based Automated Reasoning for AWS Access Policies using SMT
Barrett, Clark	CoSA: Integrated Verification for Agile Hardware Design
Baumgartner, Jason	k-FAIR = k-LIVENESS + FAIR: Revisiting SAT-based Liveness Algorithms
Becker, Heiko	A Verified Certificate Checker for Finite-Precision Error Bounds in Coq and HOL4
Bloem, Roderick	Automata Learning for Symbolic Execution Expansion-Based QBF Solving Without Recursion
Bolignano, Pauline	Semantic-based Automated Reasoning for AWS Access Policies using SMT
Braud-Santoni, Nicolas	Expansion-Based QBF Solving Without Recursion
Brunel, Julien	Analyzing the Fundamental Liveness Property of the Chord Protocol
C
Cadavero, Giuseppe	Analysis of Relay Interlocking Systems via SMT-based Model Checking of Switched Multi-Domain Kirchhoff Networks
Cadek, Pavel	Using Loop Bound Analysis For Invariant Generation
Cavada, Roberto	Analysis of Relay Interlocking Systems via SMT-based Model Checking of Switched Multi-Domain Kirchhoff Networks
Chakraborty, Supratik	Functional Synthesis via Input-Output Separation
Chemouil, David	Analyzing the Fundamental Liveness Property of the Chord Protocol
Chen, Yu-Fang	Trau: SMT solver for string constraints
Cimatti, Alessandro	Analysis of Relay Interlocking Systems via SMT-based Model Checking of Switched Multi-Domain Kirchhoff Networks
Claessen, Koen	Design-Time Railway Capacity Verification using SAT modulo Discrete Event Simulation
Cook, Byron	Semantic-based Automated Reasoning for AWS Access Policies using SMT
Cruz-Filipe, Luís	Complete and Efficient DRAT Proof Checking
D
Daly, Ross	CoSA: Integrated Verification for Agile Hardware Design
Danninger, Clemens	Using Loop Bound Analysis For Invariant Generation
Darulova, Eva	A Verified Certificate Checker for Finite-Precision Error Bounds in Coq and HOL4
Diep, Bui Phi	Trau: SMT solver for string constraints
Dodge, Catherine	Semantic-based Automated Reasoning for AWS Access Policies using SMT
E
Ebrahimi, Masoud	Automata Learning for Symbolic Execution
Egly, Uwe	Expansion-Based QBF Solving Without Recursion
Enescu, Florian	Post-Verification Debugging and Rectification of Finite Field Arithmetic Circuits using Computer Algebra Techniques
F
Fedyukovich, Grigory	Solving Constrained Horn Clauses Using Syntax and Data
Fox, Anthony	A Verified Certificate Checker for Finite-Precision Error Bounds in Coq and HOL4
Fried, Dror	Functional Synthesis via Input-Output Separation
Furbach, Florian	BMC with Memory Models as Modules
G
Gacek, Andrew	Semantic-based Automated Reasoning for AWS Access Policies using SMT
Gavran, Ivan	Learning Linear Temporal Properties
Goldberg, Eugene	Complete Test Sets And Their Approximations
Griggio, Alberto	Certifying Proofs for LTL Model Checking
Gupta, Aarti	Solving Constrained Horn Clauses Using Syntax and Data
Gupta, Aarti	Integrating Memory Consistency Models with Instruction-Level Abstraction for Heterogeneous System-on-Chip Verification
Gupta, Utkarsh	Post-Verification Debugging and Rectification of Finite Field Arithmetic Circuits using Computer Algebra Techniques
H
Hadžić, Vedad	Expansion-Based QBF Solving Without Recursion
Hanrahan, Pat	CoSA: Integrated Verification for Agile Hardware Design
Heljanko, Keijo	BMC with Memory Models as Modules
Heule, Marijn	Formal Verification of Unsatisfiability Results
Hoenicke, Jochen	Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems
Hojjat, Hossein	The Eldarica Horn Solver
Holik, Lukas	Trau: SMT solver for string constraints
Hruska, Martin	Template-Based Verification of Heap-Manipulating Programs
Huff, Dillon	CoSA: Integrated Verification for Agile Hardware Design
I
Ilioaea, Irina	Post-Verification Debugging and Rectification of Finite Field Arithmetic Circuits using Computer Algebra Techniques
Ivrii, Alexander	k-FAIR = k-LIVENESS + FAIR: Revisiting SAT-based Liveness Algorithms
J
Johansen, Christian	Design-Time Railway Capacity Verification using SAT modulo Discrete Event Simulation
K
Kalla, Priyank	Post-Verification Debugging and Rectification of Finite Field Arithmetic Circuits using Computer Algebra Techniques
L
Leino, Rustan	Semantic-based Automated Reasoning for AWS Access Policies using SMT
Lonsing, Florian	Expansion-Based QBF Solving Without Recursion
Luckow, Kasper	Semantic-based Automated Reasoning for AWS Access Policies using SMT
Luteberget, Bjørnar	Design-Time Railway Capacity Verification using SAT modulo Discrete Event Simulation
M
Madhukar, Kumar	Solving Constrained Horn Clauses Using Syntax and Data
Malik, Sharad	Integrating Memory Consistency Models with Instruction-Level Abstraction for Heterogeneous System-on-Chip Verification
Malík, Viktor	Template-Based Verification of Heap-Manipulating Programs
Manerkar, Yatin	Integrating Memory Consistency Models with Instruction-Level Abstraction for Heterogeneous System-on-Chip Verification
Mann, Makai	CoSA: Integrated Verification for Agile Hardware Design
Martinelli Tabajara, Lucas	Functional Synthesis via Input-Output Separation
Martonosi, Margaret	Integrating Memory Consistency Models with Instruction-Level Abstraction for Heterogeneous System-on-Chip Verification
Mattarei, Cristian	CoSA: Integrated Verification for Agile Hardware Design
McMillan, Kenneth L.	Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems
Meyer, Roland	BMC with Memory Models as Modules
Monat, Raphaël	A Verified Certificate Checker for Finite-Precision Error Bounds in Coq and HOL4
Mover, Sergio	Analysis of Relay Interlocking Systems via SMT-based Model Checking of Switched Multi-Domain Kirchhoff Networks
Myreen, Magnus O.	A Verified Certificate Checker for Finite-Precision Error Bounds in Coq and HOL4
N
Narodytska, Nina	Formal Verification of Deep Neural Networks
Neider, Daniel	Learning Linear Temporal Properties
Nevo, Ziv	k-FAIR = k-LIVENESS + FAIR: Revisiting SAT-based Liveness Algorithms
P
Padon, Oded	Deductive Verification of Distributed Protocols in First-Order Logic Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems
Pani, Thomas	Rely-Guarantee Reasoning for Automated Bound Analysis of Lock-Free Algorithms
Passmore, Grant	Formal Verification of Financial Algorithms with Imandra
Podelski, Andreas	Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems
Polikarpova, Nadia	Automatic Synchronization for GPU Kernels
Ponce-De-Leon, Hernan	BMC with Memory Models as Modules
Prabhu, Sumanth	Solving Constrained Horn Clauses Using Syntax and Data
R
Rao, Vikas	Post-Verification Debugging and Rectification of Finite Field Arithmetic Circuits using Computer Algebra Techniques
Rebola Pardo, Adrian	Complete and Efficient DRAT Proof Checking
Rezine, Ahmed	Trau: SMT solver for string constraints
Rosu, Grigore	Formal Design, Implementation and Verification of Blockchain Languages
Roveri, Marco	Certifying Proofs for LTL Model Checking
Ruemmer, Philipp	Bit-Vector Interpolation and Quantifier Elimination by Lazy Reduction The Eldarica Horn Solver Trau: SMT solver for string constraints
Rungta, Neha	Semantic-based Automated Reasoning for AWS Access Policies using SMT
S
Sagiv, Mooly	Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems
Scaglione, Giuseppe	Analysis of Relay Interlocking Systems via SMT-based Model Checking of Switched Multi-Domain Kirchhoff Networks
Schrammel, Peter	Template-Based Verification of Heap-Manipulating Programs
Seidl, Martina	Expansion-Based QBF Solving Without Recursion
Sessa, Mirko	Analysis of Relay Interlocking Systems via SMT-based Model Checking of Switched Multi-Domain Kirchhoff Networks
Shoham, Sharon	Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems
Sinn, Moritz	Using Loop Bound Analysis For Invariant Generation
Srinath, Arpitha	Post-Verification Debugging and Rectification of Finite Field Arithmetic Circuits using Computer Algebra Techniques
T
Tappler, Martin	Automata Learning for Symbolic Execution
Tawa, Jeanne	Analyzing the Fundamental Liveness Property of the Chord Protocol
Tkachuk, Oksana	Semantic-based Automated Reasoning for AWS Access Policies using SMT
Tonetta, Stefano	Certifying Proofs for LTL Model Checking
Trippel, Caroline	Integrating Memory Consistency Models with Instruction-Level Abstraction for Heterogeneous System-on-Chip Verification
V
Vardi, Moshe	Functional Synthesis via Input-Output Separation
Varming, Carsten	Semantic-based Automated Reasoning for AWS Access Policies using SMT
Vojnar, Tomas	Template-Based Verification of Heap-Manipulating Programs
W
Weissenbacher, Georg	Rely-Guarantee Reasoning for Automated Bound Analysis of Lock-Free Algorithms
Winter, Johannes	Automata Learning for Symbolic Execution
Z
Zeljić, Aleksandar	Bit-Vector Interpolation and Quantifier Elimination by Lazy Reduction
Zhang, Hongce	Integrating Memory Consistency Models with Instruction-Level Abstraction for Heterogeneous System-on-Chip Verification
Zuleger, Florian	Rely-Guarantee Reasoning for Automated Bound Analysis of Lock-Free Algorithms Using Loop Bound Analysis For Invariant Generation
Zyuzin, Nikita	A Verified Certificate Checker for Finite-Precision Error Bounds in Coq and HOL4

Disclaimer | Powered by EasyChair Smart Program