Formal Methods in Computer-Aided Design (FMCAD)No Descriptionhttps://hdl.handle.net/2152/20058https://repositories.lib.utexas.edu/retrieve/13b4aeed-8cb0-4df9-80ed-af5ec3e2ff2a/2024-04-19T00:26:51Z2024-04-19T00:26:51Z181Proceedings of Formal Methods in Computer-Aided Design, FMCAD 2023Formal Methods in Computer Aided Designhttps://hdl.handle.net/2152/1222152023-10-31T22:02:37Z2023-01-01T00:00:00Zdc.title: Proceedings of Formal Methods in Computer-Aided Design, FMCAD 2023
dc.description: The Conference on Formal Methods in Computer-Aided Design (FMCAD) is an annual conference on the theory and applications of formal methods in hardware and system in academia and industry for presenting and discussing groundbreaking methods, technologies, theoretical results, and tools for reasoning formally about computing systems. FMCAD covers formal aspects of computer-aided system testing.; Table of Contents: INVITED TALKS -- Reasoning about Quantifiers in SMT: The QSMA Algorithm / by Maria Paola Bonacina (p. 1) -- Distribution Testing: The New Frontier for Formal Methods / by Kuldeep Meel (p. 2) -- Formal Methods for Trusted AI / by Bettina Könighofer (p. 3) -- TUTORIALS -- Developing an Open-Source, State-of-the-Art Symbolic Model-Checking Framework for the
Model-Checking Research Community / by Kristin Y. Rozier, Natarajan Shankar, Cesare Tinelli, Moshe Vardi (p. 4) -- MiniZinc for Formal Methods / by Peter J. Stuckey (p. 5) -- Local Search and Its Application in CDCL/CDCL(T) solvers for SAT/SMT / by Shaowei Cai (p. 6) -- NASA’s core Flight System Framework Overview / by David Swartwout (p. 7) -- STUDENT FORUM -- The FMCAD 2022 Student Forum / by Mikoláš Janota, Nina Narodytska (p. 8) -- NEURAL NETWORKS AND MACHINE LEARNING -- Formally Explaining Neural Networks within Reactive Systems / by Shahaf Bassan, Guy Amir, Davide Corsi, Idan Refaeli, and Guy Katz (p. 10) -- Lightweight Online Learning for Sets of Related Problems in Automated Reasoning / by Haoze Wu, Christopher Hahn, Florian Lonsing, Makai Mann, Raghuram Ramanujan, and Clark
Barrett (p. 23) -- DelBugV: Delta-Debugging Neural Network Verifiers / by Raya Elsaleh and Guy Katz (p. 34) -- MODEL CHECKING -- Towards Compositional Hardware Model Checking Certification / by Emily Yu, Nils Froleyks, Armin Biere, and Keijo Heljanko (p. 44) -- Btor2MLIR: A Format and Toolchain for Hardware Verification / by Joseph Tafese, Isabel Garcia-Contreras, and Arie Gurfinkel (p. 55) -- Data-Driven Learning of Strong Conjunctive Invariants / by Arkesh Thakkar and Deepak D’Souza (p. 64) -- Automating Cutoff-based Verification of Distributed Protocols / by Shreesha G. Bhat and Kartik Nagar (p. 75) -- Optimal Bounded Partial Order Reduction / by Iason Marmanis and Viktor Vafeiadis (p. 86) -- HARDWARE -- Datapath Verification via Word-Level E-Graph Rewriting / by Samuel Coward, Emiliano Morini, Bryan Tan, Theo Drane, and George A. Constantinides (p. 92) -- µArchiFI: Formal Modeling and Verification Strategies for Microarchitetural Fault Injections / by Simon Tollec, Mihail Asavoae, Damien Couroussé, Karine Heydemann, and Mathieu Jan (p. 101) -- Sylvia: Countering the Path Explosion Problem in the Symbolic Execution of Hardware Designs / by Kaki Ryan and Cynthia Sturton (p. 110) -- Binary decision diagrams on modern hardware / by Samuel Pastva and Thomas Henzinger (p. 122) -- SAT -- Proofs for Incremental SAT with Inprocessing / by Benjamin Kiesl-Reiter and Michael W. Whalen (p. 132) -- Verified Encodings for SAT Solvers / by Cayden R. Codel, Jeremy Avigad, and Marijn J. H. Heule (p. 141) -- SAT-Based Quantified Symmetric Minimization of the Reachable States of Distributed Protocols / by Katalin Fazekas, Aman Goel, and Karem A. Sakallah (p. 152) -- BIG Backbones / by Nils Froleyks, Emily Yu, and Armin Biere (p. 162) -- SMT -- Local Search For SMT On Linear and Multilinear Real Arithmetic / by Bohan Li and Shaowei Cai (p. 168) -- Mariposa: Measuring SMT Instability in Automated Program Verification / by Yi Zhou, Jay Bosamiya, Yoshiki Takashima, Jessica Li, Marijn J. H. Heule, and Bryan Parno (p. 178) -- A Procedure for SyGuS Solution Fitting via Matching and Rewrite Rule Discovery / by Abdalrhman Mohamed, Andrew Reynolds, Clark Barrett, and Cesare Tinelli (p. 189) -- Partitioning Strategies for Distributed SMT Solving / by Amalee Wilson, Andres Noetzli, Andrew Reynolds, Byron Cook, Cesare Tinelli, and Clark Barrett (p. 199) -- AVIONICS -- CRV: An Automated Resiliency Reasoner for System Design Models / by Daniel Larraz, Robert Lorch, Moosa Yahyazadeh, M. Fareed Arif, Omar Chowdhury, and
Cesare Tinelli (p. 209) -- Towards a Correct-by-Construction Design of Integrated Modular Avionics / by Baoluo Meng, Joyanta Debnath, Sarat Chandra Varanasi, Emmanuel Manolios, Michael
Durling, Saswata Paul, Daniel Prince, Saif Alsabbagh, Richard Haadsma, Craig McMillan, Chi
Zhang, and Tim Oates (p. 221) -- Fortis: A Tool for Analysis and Repair of Robust Software Systems / by Changjian Zhang, Ian Dardik, Rômulo Meira-Góes, David Garlan, and Eunsuk Kang (p. 228) -- A provably correct floating-point implementation of Well Clear Avionics Concepts / by Nikson Bernardes Fernandes Ferreira, Mariano M. Moscato, Laura Titolo, and Mauricio
Ayala-Rincón (p. 237) -- SECURITY AND SYNTHESIS -- Formal Verification of Correctness and Information Flow Security for an In-Order Pipelined
Processor / by Ning Dong, Roberto Guanciale, Mads Dam, and Andreas Lööw (p. 247) -- Modular System Synthesis / by Kanghee Park, Keith J. C. Johnson, Loris D’Antoni, and Thomas Reps (p. 257) -- Modelling and Verification of Security-Oriented Resource Partitioning Schemes / by Adwait Godbole, Leiqi Ye, Yatin A. Manerkar, and Sanjit A. Seshia (p. 268) -- CYBER-PHYSICAL SYSTEMS -- Lift-off: Trustworthy ARMv8 semantics from formal specifications / by Kait Lam and Nicholas Coughlin (p. 274) -- Cycle and Commute: Rare-Event Probability Verification for Chemical Reaction Networks / by Landon Taylor, Bryant Israelsen, and Zhen Zhang (p. 284) -- Conformance Testing for Stochastic Cyber-Physical Systems / by Xin Qin, Navid Hashemi, Lars Lindemann, Jyotirmoy V. Deshmukh (p. 294) -- MediK: Towards Safe Guideline-based Clinical Decision Support / by Manasvi Saxena, Shuang Song, and Lui Sha (p. 306)
2023-01-01T00:00:00ZProceedings of Formal Methods in Computer-Aided Design, FMCAD 2022Formal Methods in Computer Aided Designhttps://hdl.handle.net/2152/1174802023-02-17T09:02:48Z2022-01-01T00:00:00Zdc.title: Proceedings of Formal Methods in Computer-Aided Design, FMCAD 2022
dc.contributor.editor: Griggio, Alberto; Rungta, Neha
dc.description: The Conference on Formal Methods in Computer-Aided Design (FMCAD) is an annual conference on the theory and applications of formal methods in hardware and system verification. FMCAD provides a leading forum to researchers in academia and industry for presenting and discussing groundbreaking methods, technologies, theoretical results, and tools for reasoning formally about computing systems. FMCAD covers formal aspects of computer-aided system design including verification, specification, synthesis, and testing.; Table of Contents: Invited Talks -- The seL4 Verification Journey: How Have the Challenges and Opportunities Evolved / by June Andronick (p. 1) -- Why Do Things Go Wrong (or Right)? Applications of Causal Reasoning to Verification / by Hana Chockler (p. 2) -- Tutorials -- On Applying Model Checking in Formal Verification / by Håkan Hjort (p. 3) -- Verification of Distributed Protocols: Decidable Modeling and Invariant Inference / by Oded Padon (p. 4) -- Student Forum -- The FMCAD 2022 Student Forum / by Matthias Preiner (p. 5) -- Verification in Machine Learning -- Proving Robustness of KNN Against Adversarial Data Poisoning / by Yannan Li, Jingbo Wang and Chao Wang (p. 7) -- On Optimizing Back-Substitution Methods for Neural Network Verification / by Tom Zelazny, Haoze Wu, Clark Barrett and Guy Katz (p. 17) -- Verification-Aided Deep Ensemble Selection ./ by Guy Amir, Tom Zelazny, Guy Katz and Michael Schapira (p. 27) -- Neural Network Verification with Proof Production / by Omri Isac, Clark Barrett, Min Zhang and Guy Katz (p. 38) -- Proofs -- TBUDDY: A Proof-Generating BDD Package / by Randal Bryant (p. 49) -- Stratified Certification for k-Induction / by Emily Yu, Nils Frolyeks, Armin Biere and Keijo Heljanko (p. 59) -- Reconstructing Fine-Grained Proofs of Complex Rewrites Using a Domain-Specific Language / by Andres Noetzli, Haniel Barbosa, Aina Niemetz, Mathias Preiner, Andrew Reynolds, Cesare
Tinelli and Clark Barrett (p. 65) -- Small Proofs from Congruence Closure / by Oliver Flatt, Samuel Coward, Max Willsey, Zachary Tatlock and Pavel Panchekha (p. 75) -- Proof-Stitch: Proof Combination for Divide-and-Conquer SAT Solvers / by Abhishek Nair, Saranyu Chattopadhyay, Haoze Wu, Alex Ozdemir and Clark Barrett (p. 84) -- Hardware and RTL -- Reconciling Verified-Circuit Development and Verilog Development / by Andreas Lööw (p. 89) -- Timed Causal Fanin Analysis for Symbolic Circuit Simulation / by Roope Kaivola and Neta Bar Kama (p. 99) -- Divider Verification Using Symbolic Computer Algebra and Delayed Don’t Care Optimization / by Alexander Konrad, Christoph Scholl, Alireza Mahzoon, Daniel Große and Rolf Drechsler (p. 108) -- Formally Verified Isolation of DMA / by Jonas Haglund and Roberto Guanciale (p. 118) -- Foundations and Tools in HOL4 for Analysis of Microarchitectural Out-of-Order Execution / by Karl Palmskog, Xiaomo Yao, Ning Dong, Roberto Guanciale and Mads Dam (p. 129) -- Synthesizing Instruction Selection Rewrite Rules from RTL using SMT / by Ross Daly, Caleb Donovick, Jack Melchert, Raj Setaluri, Nestan Tsiskaridze, Priyanka Raina,
Clark Barrett and Pat Hanrahan (p. 139) -- Error Correction Code Algorithm and Implementation Verification using Symbolic Representations / by Aarti Gupta, Roope Kaivola, Mihir Parang Mehta and Vaibhav Singh (p. 151) -- SAT and SMT -- First-Order Subsumption via SAT Solving / by Jakob Rath, Armin Biere and Laura Kovacs (p. 160) -- BaxMC: a CEGAR approach to MAX#SAT / by Thomas Vigouroux, Cristian Ene, David Monniaux, Laurent Mounier and Marie-Laure Potet (p. 170) -- Compact Symmetry Breaking for Tournaments / by Evan Lohn, Chris Lambert and Marijn Heule (p. 179) -- Enumerative Data Types with Constraints / by Andrew T Walter, David Greve and Panagiotis Manolios (p. 189) -- Reducing NEXP-complete problems to DQBF / by Fa-Hsun Chen, Shen-Chang Huang, Yu-Cheng Lu and Tony Tan (p. 199) -- INC: A Scalable Incremental Weighted Sampler / by Suwei Yang, Victor Liang and Kuldeep S. Meel (p. 205) -- Bounded Model Checking for LLVM / by Siddharth Priya, Xiang Zhou, Yusen Su, Yakir Vizel, Yuyan Bao and Arie Gurfinkel (p. 214) -- Parameterized Systems and Quantified Reasoning -- Automatic Repair and Deadlock Detection for Parameterized Systems / by Swen Jacobs, Mouhammad Sakr and Marcus Völp (p. 225) -- Synthesizing Locally Symmetric Parameterized Protocols from Temporal Specifications / by Ruoxi Zhang, Richard Trefler and Kedar Namjoshi (p. 235) -- Synthesizing Self-Stabilizing Parameterized Protocols with Unbounded Variables / by Ali Ebnenasir (p. 245) -- The Rapid Software Verification Framework / by Pamina Georgiou, Bernhard Gleiss, Ahmed Bhayat, Michael Rawson, Laura Kovacs and Giles
Reger (p. 255) -- Distributed Systems -- ACORN: Network Control Plane Abstraction using Route Nondeterminism / by Divya Raghunathan, Ryan Beckett, Aarti Gupta and David Walker (p. 261) -- Plain and Simple Inductive Invariant Inference for Distributed Protocols in TLA+ / by William Schultz, Ian Dardik and Stavros Tripakis (p. 273) -- Awaiting for Godot: Stateless Model Checking that Avoids Executions where Nothing Happens / by Bengt Jonsson, Magnus Lång and Kostis Sagonas (p. 284) -- Synthesis -- Synthesizing Transducers from Complex Specifications / by Anvay Grover, Rüdiger Ehlers and Loris D’Antoni (p. 294) -- Synthesis of Semantic Actions in Attribute Grammars / by Pankaj Kumar Kalita, Miriyala Jeevan Kumar and Subhajit Roy (p. 304) -- Reactive Synthesis Modulo Theories using Abstraction Refinement / by Benedikt Maderbacher and Roderick Bloem (p. 315) -- Learning Deterministic Finite Automata Decompositions from Examples and Demonstrations / by Niklas Lauffer, Beyazit Yalcinkaya, Marcell Vazquez-Chanlatte, Ameesh Shah and Sanjit A. Seshia (p. 325) -- Reachability and Safety Verification -- Automated Conversion of Axiomatic to Operational Models: Theoretical and Practical Results / by Adwait Godbole, Yatin A. Manerkar and Sanjit A. Seshia (p. 331) -- Formally Verified Quite OK Image Format / by Mario Bucev and Viktor Kunčak (p. 343) -- Split Transition Power Abstraction for Unbounded Safety / by Martin Blicha, Grigory Fedyukovich, Antti Hyvärinen and Natasha Sharygina (p. 349) -- Automating Geometric Proofs of Collision Avoidance with Active Corners / by Nishant Kheterpal, Elanor Tang and Jean-Baptiste Jeannin (p. 359) -- Differential Testing of Pushdown Reachability with a Formally Verified Oracle / by Anders Schlichtkrull, Morten Konggaard Schou, Jiri Srba and Dmitriy Traytel (p. 369) -- TriCera: Verifying C Programs Using the Theory of Heaps / by Zafer Esen and Philipp Ruemmer (p. 380)
2022-01-01T00:00:00ZProceedings of Formal Methods in Computer-Aided Design, FMCAD 2021Formal Methods in Computer Aided Designhttps://hdl.handle.net/2152/899702021-11-05T07:38:14Z2021-01-01T00:00:00Zdc.title: Proceedings of Formal Methods in Computer-Aided Design, FMCAD 2021
dc.contributor.editor: Piskac, Ruzica; Whalen, Michael W.
dc.description: Table of Contents: Tutorials -- Reactive Synthesis Beyond Realizability / by Rayna Dimitrova (p. 1) -- Stainless Verification System Tutorial / by Viktor Kuncak and Jad Hamza (p. 2) -- Formal Methods for the Security Analysis of Smart Contracts / by Matteo Maffei (p. 8) -- Active Automata Learning: from L* to L# / by Frits Vaandrager (p. 9) -- Invited Talks -- From Viewstamped Replication to Blockchains / by Barbara Liskov (p. 10) -- Algorithms for the People / by Seny Kamara (p. 11) -- Engineering with Full-scale Formal Architecture: Morello, CHERI, Armv8-A, and RISC-V / by Peter Sewell (p. 12) -- Student Forum -- The FMCAD 2021 Student Forum / by Mark Santolucito (p. 13) -- Hardware -- CocoAlma: A Versatile Masking Verifier / by Vedad Hadžic and Roderick Bloem (p. 14) -- End-to-End Formal Verification of a RISC-V Processor Extended with Capability Pointers / by Dapeng Gao and Tom Melham (p. 24) -- Hardware Security Leak Detection by Symbolic Simulation / by Neta Bar Kama and Roope Kaivola (p. 34) -- Scaling up Hardware Accelerator Verification using A-QED with Functional Decomposition / by
Saranyu Chattopadhyay, Florian Lonsing, Luca Piccolboni, Deepraj Soni, Peng Wei, Xiaofan
Zhang, Yuan Zhou, Luca Carloni, Deming Chen, Jason Cong, Ramesh Karri, Zhiru Zhang,
Caroline Trippel, Clark Barrett and Subhasish Mitra (p. 42) -- Sound and Automated Verification of Real-World RTL Multipliers / by Mertcan Temel and Warren Hunt (p. 53) -- Model Checking and IC3 -- IC3 with Internal Signals / by Rohit Dureja, Arie Gurfinkel, Alexander Ivrii and Yakir Vizel (p. 63) -- Single Clause Assumption without Activation Literals to Speed-up IC3 / by Nils Froleyks and Armin Biere (p. 72) -- Logical Characterization of Coherent Uninterpreted Programs / by Hari Govind Vediramana Krishnan, Sharon Shoham and Arie Gurfinkel (p. 77) -- Data-driven Optimization of Inductive Generalization / by Nham Le, Xujie Si, and Arie Gurfinkel (p. 86) -- Model Checking AUTOSAR Components with CBMC / by Timothee Durand, Katalin Fazekas, Georg Weissenbacher and Jakob Zwirchmayr (p. 96) -- Concurrency and Distributed Systems -- Automating System Configuration / by Nestan Tsiskaridze, Maxwell Strange, Makai Mann, Kavya Sreedhar, Qiaoyi Liu, Mark Horowitz and Clark Barrett (p. 102) -- Towards an Automated Proof of Lamport's Paxos / by Aman Goel and Karem A. Sakallah (p. 112) -- Refinement-Based Verification of Device-to-Device Information Flow / by Ning Dong, Roberto Guanciale, and Mads Dam (p. 123) -- Celestial: A Smart Contracts Verification Framework / by Samvid Dharanikota, Suvam Mukherjee, Chandrika Bhardwaj, Aseem Rastogi and Akash Lal (p. 133) -- The Civl Verifier / by Bernhard Kragl and Shaz Qadeer (p. 143) -- Applied Verification and Synthesis -- Synthesizing Pareto-Optimal Interpretations for Black-Box Models / by Hazem Torfah, Shetal Shah, Supratik Chakraborty, S. Akshay and Sanjit A. Seshia (p. 153) -- Dynamic Partial Order Reduction for Spinloops / by Michalis Kokologiannakis, Xiaowei Ren and Viktor Vafeiadis (p. 163) -- Robustness Between Weak Memory Models / by Soham Chakraborty (p. 173) -- Pruning and Slicing Neural Networks using Formal Verification / by Ori Lahav and Guy Katz (p. 183) -- Towards Scalable Verification of Deep Reinforcement Learning / by Guy Amir, Michael Schapira, and Guy Katz (p. 193) -- SAT Solving -- Exploiting Isomorphic Subgraphs in SAT / by Alexander Ivrii and Ofer Strichman (p. 204) -- On Decomposition of Maximal Satisfiable Subsets / by Jaroslav Bendı ́k (p. 212) -- Designing Samplers is Easy: The Boon of Testers / by Priyanka Golia, Mate Soos, Sourav Chakraborty and Kuldeep S. Meel (p. 222) -- SAT-Inspired Eliminations for Superposition / by Petar Vukmirović, Jasmin Blanchette and Marijn Heule (p. 231) -- SAT Solving in the Serverless Cloud / by Alex Ozdemir, Haoze Wu, and Clark Barrett (p. 241) -- SMT and First-Order Logic -- Induction with Recursive Definitions in Superposition / by Marton Hajdu, Petra Hozzová, Laura Kovacs and Andrei Voronkov (p. 246) -- Fair and Adventurous Enumeration of Quantifier Instantiations / by Mikolas Janota, Haniel Barbosa, Pascal Fontaine and Andrew Reynolds (p. 256) -- Mathematical Programming Modulo Strings / by Ankit Kumar and Panagiotis Manolios (p. 261) -- Lookahead in Partitioning SMT / by
Antti Hyvärinen, Matteo Marescotti and Natasha Sharygina (p. 271) -- A Multithreaded Vampire with Shared Persistent Grounding / by Michael Rawson and Giles Reger (p. 280)
2021-01-01T00:00:00ZProceedings of Formal Methods in Computer-Aided Design, FMCAD 2020Formal Methods in Computer Aided Designhttps://hdl.handle.net/2152/835612020-11-05T08:32:05Z2020-01-01T00:00:00Zdc.title: Proceedings of Formal Methods in Computer-Aided Design, FMCAD 2020
dc.contributor.editor: Ivrii, Alexander; Strichman, Ofer
dc.description: Table of Contents: Anytime Algorithms for MaxSAT and Beyond / by Alexander Nadel (p. 1) -- Formal Verification for Natural and Engineered Biological Systems / by Hillel Kugler (p. 2) -- Tutorial on World-Level Model Checking / by Armin Biere (p. 3) -- How Testable is Business Software? / by Peter Schrammel (p. 4) -- From Correctness to High Quality / by Orna Kupferman (p. 5) -- The FMCAD 2020 Student Forum / Peter Schrammel (p. 6) -- Effective System Level Liveness Verification / by Alexander Fedotov, Jeroen J.A. Keiren, and Julien Schmaltz (p. 7) -- Accelerating Parallel Verification via Complementary Property Partitioning and Strategy Exploration / by Rohit Dureja, Jason Baumgartner, Robert Kanzelman, Mark Williams, and Kristin Yvonne Rozier (p. 16) -- A Theoretical Framework for Symbolic Quick Error Detection / by Florian Lonsing, Subhasish Mitra, and Clark Barrett (p. 26) -- Runtime Verification on FPGAs and LTLf Specifications / by Tommy Tracy II, Lucas Tabajara, Moshe Vardi, and Kevin Skadron (p. 36) -- Distributed Bounded Model Checking / by Prantik Chatterjee, Subhajit Roy, Bui Phi Diep, and Akash Lal (p. 47) -- EUFicient Reachability for Software with Arrays / by Denis Bueno, Arlen Cox, and Karem A. Sakallah (p. 57) -- Thread-modular Counter Abstraction for Parameterized Program Safety / by Thomas Pani, Georg Weissenbacher, and Florian Zuleger (p. 67) -- Incremental Verification by SMT-based Summary Repair / by Sepideh Asadi, Martin Blicha, Antti Hyvärinen, Grigory Fedyukovich, and Natasha Sharygina (p. 77) -- Reactive Synthesis from Extended Bounded Response LTL Specifications / by Alessandro Cimatti, Luca Geatti, Nicola Gigante, Angelo Montanari, and Stefano Tonetta (p. 83) -- SYSLITE: Syntax-Guided Synthesis of PLTL Formulas from Finite Traces / by M. Fareed Arif, Daniel Larraz, Mitziu Echeverria, Andrew Reynolds, Omar Chowdhury, and Cesare Tinelli (p. 93) -- Learning Properties in LTL ∩ ACTL from Positive Examples Only / by Rüdiger Ehlers, Ivan Gavran, and Daniel Neider (p. 104) -- Automating Compositional Analysis of Authentication Protocols / by Zichao Zhang, Arthur Azevedo de Amorim, Limin Jia, and Corina Pasareanu (p. 113) -- Selecting Stable Safe Configurations for Systems Modelled by Neural Networks with ReLU Activation / by Franz Brauße, Zurab Khasidashvili, and Konstantin Korovin (p. 119) -- Parallelization Techniques for Verifying Neural Networks / by Haoze Wu, Alex Ozdemir, Aleksandar Zeljić, Kyle Julian, Ahmed Irfan, Divya Gopinath, Sadjad Fouladi, Guy Katz, Corina Pasareanu, and Clark Barrett (p. 128) -- Formal Methods with a Touch of Magic / by Parand Alizadeh Alamdari, Guy Avni, Thomas A. Henzinger, and Anna Lukina (p. 138) -- ART: Abstraction Refinement-Guided Training for Provably Correct Neural Networks / by Xuankang Lin, He Zhu, Roopsha Samanta, and Suresh Jagannathan (p. 148) -- Automating Modular Verification of Secure Information Flow / by Lauren Pick, Grigory Fedyukovich, and Aarti Gupta (p. 158) -- Angelic Checking within Static Driver Verifier: Towards High-precision Defects without (modeling) Cost / by Shuvendu Lahiri, Akash Lal, Sridhar Gopinath, Alexander Nutz, Vladimir Levin, Rahul Kumar, Nate Deisinger, Jakob Lichtenberg, and Chetan Bansal (p. 169) -- Model Checking Software-Defined Networks with Flow Entries that Time Out / by Vasileios Klimis, George Parisis, and Bernhard Reus (p. 179) -- Using Model Checking Tools to Triage the Severity of Security Bugs in the Xen Hypervisor / by Byron Cook, Bjoern Doebel, Daniel Kroening, Norbert Manthey, Martin Pohlack, Elizabeth Polgreen, Michael Tautschnig, and Pawel Wieczorkiewicz (p. 185) -- Verifying Properties of Bit-vector Multiplication Using Cutting Planes Reasoning / by Vincent Liew, Paul Beame, Jo Devriendt, Jan Elffers, and Jakob Nordstrom (p. 194) -- On Optimizing a Generic Function in SAT / by Alexander Nadel (p. 205) -- Ternary Propagation-Based Local Search for More Bit-Precise Reasoning / by Aina Niemetz, and Mathias Preiner (p. 214) -- Reductions for Strings and Regular Expressions Revisited / by Andrew Reynolds, Andres Noetzli, Clark Barrett, and Cesare Tinelli (p. 225) -- SWITSS: Computing Small Witnessing Subsystems / by Simon Jantsch, Hans Harder, Florian Funke, and Christel Baier (p. 236) -- Smart Induction for Isabelle/HOL (Tool Paper) / by Yutaka Nagashima (p. 245) -- Trace Logic for Inductive Loop Reasoning / by Pamina Georgiou, Bernhard Gleiss, and Laura Kovacs (p. 255) -- The Proof Checkers Pacheck and Pastèque for the Practical Algebraic Calculus / by Daniela Kaufmann, Mathias Fleury, and Armin Biere (p. 264)
2020-01-01T00:00:00ZProceedings of Formal Methods in Computer-Aided Design, FMCAD 2019Formal Methods in Computer Aided Designhttps://hdl.handle.net/2152/798532020-02-06T12:11:27Z2019-01-01T00:00:00Zdc.title: Proceedings of Formal Methods in Computer-Aided Design, FMCAD 2019
dc.contributor.editor: Barrett, Clark; Yang, Jin
dc.description: Table of Contents: Boosting Verification Scalability via Structural Grouping and Semantic Partitioning of
Properties / by Rohit Dureja, Jason Baumgartner, Alexander Ivrii, Robert Kanzelman and Kristin
Yvonne Rozier (p. 1) -- Input Elimination Transformations for Scalable Verification and Trace Reconstruction / by Raj Kumar Gajavelly, Jason Baumgartner, Alexander Ivrii, Robert Kanzelman and
Shiladitya Ghosh (p. 10) -- Chasing Minimal Inductive Validity Cores in Hardware Model Checking / by Ryan Berryhill and Andreas Veneris (p. 19) -- Verifying Large Multipliers by Combining SAT and Computer Algebra / by Daniela Kaufmann, Armin Biere and Manuel Kauers (p. 28) -- Unification-based Pointer Analysis without Oversharing / by Jakub Kuderski, Jorge A. Navas and Arie Gurfinkel (p. 37) -- Concurrent Chaining Hash Maps for Software Model Checking / by Freark I. van der Berg and Jaco van de Pol (p. 46) -- Proving Data Race Freedom in Task Parallel Programs with a Weaker Partial Order / by Benjamin Ogles, Peter Aldous and Eric Mercer (p. 55) -- BDD-Based Algorithms for Packet Classification / by Nina Narodytska, Leonid Ryzhyk, Igor Ganichev and Soner Sevinc (p. 64) -- TSNsched: Automated Schedule Generation for Time Sensitive Networking / by Aellison Cassimiro Teixeira Dos Santos, Ben Schneider and Vivek Nigam (p. 69) -- Verification and Synthesis of Symmetric Uni-Rings for Leads-To Properties / by Ali Ebnenasir (p. 78) -- Scalable Translation Validation of Unverified Legacy OS Code / by Amer Tahat, Sarang Joshi, Pronnoy Goswami and Binoy Ravindran (p. 87) -- Kaizen: Building a Performant Blockchain System Verified for Consensus and Integrity / by Faria Kalim, Karl Palmskog, Jayasi Mehar, Adithya Murali, Indranil Gupta and P.
Madhusudan (p. 96) -- KAIROS: Incremental Verification in High-Level Synthesis through Latency-Insensitive
Design / by Luca Piccolboni, Giuseppe Di Guglielmo and Luca Carloni (p. 105) -- Verification of Authenticated Firmware Loaders / by Sujit Kumar Muduli, Pramod Subramanyan and Sayak Ray (p. 110) -- Learning-Based Synthesis of Safety Controllers / by Daniel Neider and Oliver Markgraf (p. 120) -- Shield Synthesis for Real: Enforcing Safety in Cyber-Physical Systems / by Meng Wu, Jingbo Wang, Jyotirmoy Deshmukh and Chao Wang (p. 129) -- Syntroids: Synthesizing a Game for FPGAs using Temporal Logic Specifications / by Gideon Geier, Philippe Heim, Felix Klein and Bernd Finkbeiner (p. 138) -- Synthesizing Reactive Systems Using a Robustness Specification / by Roderick Bloem, Hana Chockler, Masoud Ebrahimi and Ofer Strichman (p. 147) -- Property Directed Inference of Relational Invariants / by Dmitry Mordvinov and Grigory Fedyukovich (p. 152) -- Knowledge Compilation for Boolean Functional Synthesis / by S. Akshay, Jatin Arora, Supratik Chakraborty, Krishna S, Divya Raghunathan and
Shetal Shah (p. 161) -- Verifying Relational Properties using Trace Logic / by Gilles Barthe, Renate Eilers, Pamina Georgiou, Bernhard Gleiss, Laura Kovacs and
Matteo Maffei (p. 170) -- Autarkies for DQCNF / by Oliver Kullmann and Ankit Shukla (p. 179) -- Localizing Quantifiers for DQBF / by Aile Ge-Ernst, Christoph Scholl and Ralf Wimmer (p. 184) -- Anytime Weighted MaxSAT with Improved Polarity Selection and Bit-Vector
Optimization / by Alexander Nadel (p. 193) -- GuidedSampler: Coverage-guided Sampling of SMT Solutions / by Rafael Dutra, Jonathan Bachrach and Koushik Sen (p. 203) -- Extending enumerative function synthesis via SMT-driven classification / by Haniel Barbosa, Andrew Reynolds, Daniel Larraz and Cesare Tinelli (p. 212) -- Proving Non-Termination via Loop Acceleration / by Florian Frohn and Jürgen Giesl (p. 221)
2019-01-01T00:00:00ZProceedings of Formal Methods in Computer Aided Design, FMCAD 2018Formal Methods in Computer Aided Designhttps://hdl.handle.net/2152/750602019-07-06T08:00:56Z2018-01-01T00:00:00Zdc.title: Proceedings of Formal Methods in Computer Aided Design, FMCAD 2018
dc.contributor.editor: Bjørner, Nikolaj; Gurfinkel, Arie
dc.description: October 30 – November 2, 2018 in Austin, Texas, USA; Table of Contents: INVITED PAPERS -- Formal Verification of Deep Neural Networks / by Nina Narodytska (p. 1) -- Formal Verification of Unsatisfiability Results / by Marijn Heule (p. 2) -- Deductive Verification of Distributed Protocols in First-Order Logic / by Oded Padon (p. 3) -- Formal Verification of Financial Algorithms with Imandra / by Grant Passmore (p. 4) -- Formal Design, Implementation and Verification of Blockchain Languages / by Grigore Rosu (p. 5) -- The FMCAD 2018 Graduate Student Forum / by Dejan Jovanović and Andrew Reynolds (p. 6) -- HARDWARE -- CoSA: Integrated Verification for Agile Hardware Design / by Cristian Mattarei, Makai Mann, Clark Barrett, Ross Daly, Dillon Huff, and Pat Hanrahan (p. 7) -- ILA-MCM: Integrating Memory Consistency Models with Instruction-Level Abstractions for Heterogeneous System-on-Chip Verification / by Hongce Zhang, Caroline Trippel, Yatin Manerkar, Aarti Gupta, Margaret Martonosi, and Sharad Malik (p. 12) -- BMC with Memory Models as Modules / by Hernan Ponce-De-Leon, Florian Furbach, Keijo Heljanko, and Roland Meyer (p. 22) -- QUANTIFIERS AND SAT -- Complete Test Sets and Their Approximations / by Eugene Goldberg (p. 31) -- Expansion-Based QBF Solving Without Recursion / by Roderick Bloem, Nicolas Braud-Santoni, Vedad Hadžić, Uwe Egly, Florian Lonsing, and Martina Seidl (p. 40) -- Bit-Vector Interpolation and Quantifier Elimination by Lazy Reduction / by Peter Backeman, Philipp Ruemmer, and Aleksandar Zeljić (p. 50) -- LIVENESS -- Analyzing the Fundamental Liveness Property of the Chord Protocol / by Julien Brunel, David Chemouil, and Jeanne Tawa (p. 60) -- k-FAIR = k-LIVENESS + FAIR: Revisiting SAT-based Liveness Algorithms / by Alexander Ivrii, Ziv Nevo, and Jason Baumgartner (p. 69) -- Temporal Prophecy for Proving Temporal Properties of Infinite-State Systems / by Oded Padon, Jochen Hoenicke, Kenneth L. McMillan, Andreas Podelski, Mooly Sagiv, and Sharon Shoham (p. 74) -- CONCURRENCY -- Automatic Synchronization for GPU Kernels / by Sourav Anand and Nadia Polikarpova (p. 85) -- Rely-Guarantee Reasoning for Automated Bound Analysis of Lock-Free Algorithms / by Thomas Pani, Georg Weissenbacher, and Florian Zuleger (p. 94) -- VERIFICATION -- Template-Based Verification of Heap-Manipulating Programs / by Viktor Malík, Martin Hruska, Peter Schrammel, and Tomas Vojnar (p. 103) -- Using Loop Bound Analysis for Invariant Generation / by Pavel Cadek, Clemens Danninger, Moritz Sinn, and Florian Zuleger (p. 112) -- Post-Verification Debugging and Rectification of Finite Field Arithmetic Circuits using Computer Algebra Techniques / by Vikas Rao, Utkarsh Gupta, Irina Ilioaea, Arpitha Srinath, Priyank Kalla, and Florian Enescu (p. 121) -- LEARNING AND SYNTHESIS -- Automata Learning for Symbolic Execution / by Bernhard K. Aichernig, Roderick Bloem, Masoud Ebrahimi, Martin Tappler, and Johannes Winter (p. 130) -- Functional Synthesis via Input-Output Separation / by Supratik Chakraborty, Dror Fried, Lucas Martinelli Tabajara, and Moshe Vardi (p. 139) -- Learning Linear Temporal Properties / by Ivan Gavran and Daniel Neider (p. 148) -- SMT AND CHC -- The Eldarica Horn Solver / by Hossein Hojjat and Philipp Ruemmer (p. 158) -- Trau: SMT Solver for String Constraints / by Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Bui Phi Diep, Lukas Holik, Ahmed Rezine, and Philipp Ruemmer (p. 165) -- Solving Constrained Horn Clauses Using Syntax and Data / by Grigory Fedyukovich, Sumanth Prabhu, Kumar Madhukar, and Aarti Gupta (p. 170) -- RAILS -- Analysis of Relay Interlocking Systems via SMT-based Model Checking of Switched Multi-Domain Kirchhoff Networks / by Roberto Cavada, Alessandro Cimatti, Sergio Mover, Mirko Sessa, Giuseppe Cadavero, and Giuseppe Scaglione (p. 179) -- Design-Time Railway Capacity Verification using SAT Modulo Discrete Event Simulation / by Bjørnar Luteberget, Koen Claessen, and Christian Johansen (p. 188) -- CERTIFICATES -- Complete and Efficient DRAT Proof Checking / by Adrian Rebola Pardo and Luís Cruz-Filipe (p. 197) -- Semantic-based Automated Reasoning for AWS Access Policies using SMT / by John Backes, Pauline Bolignano, Byron Cook, Catherine Dodge, Andrew Gacek, Kasper Luckow, Neha Rungta, Oksana Tkachuk, and Carsten Varming (p. 206) -- A Verified Certificate Checker for Finite-Precision Error Bounds in Coq and HOL4 / by Heiko Becker, Nikita Zyuzin, Raphaël Monat, Eva Darulova, Magnus O. Myreen, and Anthony Fox (p. 215) -- Certifying Proofs for LTL Model Checking / by Alberto Griggio, Marco Roveri, and Stefano Tonetta (p. 225)
2018-01-01T00:00:00ZProceedings of Formal Methods in Computer Aided Design, FMCAD 2017Formal Methods in Computer Aided Designhttps://hdl.handle.net/2152/628752019-02-08T20:48:59Z2017-01-01T00:00:00Zdc.title: Proceedings of Formal Methods in Computer Aided Design, FMCAD 2017
dc.contributor.editor: Stewart, Daryl; Weissenbacher, Georg
dc.description: October 2-6, 2017, in Vienna Austria; Table of Contents: Invited Papers -- How formal analysis and verification add security to blockchain-based systems / by Shin 'Ichiro Matsuo (p. 1) -- Symbolic Security Analysis using the Tamarin Prover / by Cas Cremers (p. 5) --
Coalition, intrigue, ambush, destruction and pride: herding cats can be challenging / by Jade Alglave (p. 6) -- Automated Formal Reasoning About AWS Systems / by Byron Cook (p. 7)
-- Formal Methods in Industrial Dependable Systems Design - The TTTech Example / by Wilfried Steiner (p. 8) -- Hardware Model Checking Competition 2017 / by Armin Biere, Tom van Dijk and Keijo Heljanko (p. 9) --
The FMCAD 2017 Graduate Student Forum / by Keijo Heljanko (p. 10) -- Arithmetric -- goSAT: Floating-point Satisfiability as Global Optimization / by M. Ammar Ben Khadra, Dominik Stoffel and Wolfgang Kunz
(p. 11) --
On Sound Relative Error Bounds for Floating-Point Arithmetic / by Anastasiia Izycheva and Eva Darulova
(p. 15) -- Column-Wise Verification of Multipliers Using Computer Algebra / by Daniela Ritirc, Armin Biere and Manuel Kauers (p. 23) --
Solving -- Efficient Generation of All Minimal Inductive Validity Cores / by Elaheh Ghassabani, Michael Whalen and Andrew Gacek (p. 31) -- Duality-Based Interpolation for Quantifier-Free Equalities and Uninterpreted Functions / by Leonardo Alt, Antti Hyvarinen, Sepideh Asadi and Natasha Sharygina (p. 39) --
Solving Linear Arithmetic with SAT-based Model Checking / by Yakir Vizel, Alexander Nadel and Sharad Malik (p. 47) -- Z3str3: A String Solver with Theory-aware Heuristics / by Murphy Berzish, Vijay Ganesh and Yunhui Zheng (p. 55) -- Concurrency and Distributed Systems --
Verification of a lazy cache coherence protocol against a weak memory model / by Christopher Banks, Marco Elver, Ruth Hoffmann, Susmit Sarkar, Paul Jackson and Vijay Nagarajan (p. 60) -- Safety Verification of Phaser Programs / by Zeinab Ganjei, Ahmed Rezine, Petru Eles and Zebo Peng (p. 68) --
Learning to prove safety over parameterised concurrent systems / by Yu-Fang Chen, Chih-Duo Hong, Anthony Widjaja Lin and Philipp Ruemmer (p. 76) -- Lasso detection using Partial State Caching / by Rashmi Mudduluru, Pantazis Deligiannis, Ankush Desai, Akash Lal and Shaz Qadeer (p. 84) -- Probabilistic Systems --
Exact Quantitative Probabilistic Model Checking Using Rational Search / by Matthew S. Bauer, Umang Mathur, Rohit Chadha, A. Prasad Sistla and Mahesh Viswanathan (p. 92) -- Sampling Invariants from Frequency Distributions / by Grigory Fedyukovich, Samuel Kaufman and Rastislav Bodik (p. 100) -- BDDs --
Tagged BDDs: Combining reduction rules from different decision diagram types / by Tom van Dijk, Robert Wille and Robert Meolic (p. 108) -- First-order Temporal Logic Monitoring with BDDs / by Klaus Havelund, Doron Peled and Dogan Ulus
(p. 116) --
Factored Boolean Functional Synthesis / by Lucas Martinelli Tabajara and Moshe Y. Vardi
(p. 124) -- IC3 -- Property Directed Reachability with Word-Level Abstraction / by Yen-Sheng Ho, Alan Mishchenko and Robert Brayton (p. 132) --
Learning Support Sets in IC3 and Quip: the Good, the Bad, and the Ugly / by Ryan Berryhill, Alexander Ivrii, Neil Veira and Andreas Veneris
(p. 140) -- K-Induction without Unrolling / by Arie Gurfinkel and Alexander Ivrii
(p. 148) --
Designing Parallel PDR / by Matteo Marescotti, Arie Gurfinkel, Antti Hyvarinen and Natasha Sharygina (p. 156) -- FuseIC3: An Algorithm for Checking Large Design Spaces / by Rohit Dureja and Kristin Yvonne Rozier (p. 164) --
FAR-Cubicle - A new reachability algorithm for Cubicle / by Sylvain Conchon, Amit Goel, Sava Krstic, Rupak Majumdar and Mattias Roux (p. 172) -- Theta: a Framework for Abstraction Refinement-Based Model Checking / by Tamas Toth, Akos Hajdu, Andras Voros, Zoltan Micskei and Istvan Majzik (p. 176) --
Hybrid Systems -- Modular SMT-Based Analysis of Nonlinear Hybrid Systems / by Kyungmin Bae and Sicun Gao (p. 180) -- SMT-based Analysis of Switching Multi-Domain Linear Kirchhoff Networks / by Alessandro Cimatti, Sergio Mover and Mirko Sessa
(p. 188) -- Applications --
Automatic Verification of Application-Tailored OSEK Kernels / by Hans-Peter Deifel, Christian Dietrich, Merlin Gottlinger, Daniel Lohmann, Stefan Milius and Lutz Schroder (p. 196) -- Estimating Worst-case Latency of on-chip Interconnects with Formal Simulation / by Freek Verbeek and Nike van Vugt-Hage
(p. 204) --
Parameterized Verification of Algorithms for Oblivious Robots on a Ring / by Arnaud Sangnier, Nathalie Sznajder, Maria Potop-Butucaru and Sebastien Tixeuil
(p. 212) -- Automated Repair By Example for Firewalls / by William Hallahan, Ennan Zhai and Ruzica Piskac (p. 220)
2017-01-01T00:00:00ZProceedings of Formal Methods in Computer-Aided Design, FMCAD 2016Formal Methods in Computer Aided Designhttps://hdl.handle.net/2152/437842019-02-08T20:47:15Z2016-10-01T00:00:00Zdc.title: Proceedings of Formal Methods in Computer-Aided Design, FMCAD 2016
dc.description: Table of Contents: Formal Verification for Computer Security: Lessons Learned and Future Directions / by Dawn Song (p.1) --Understanding Evolution through Algorithms / by Christos Papadimitriou (p.2) -- Network Verification - When Clarke Meets Cerf / by George Varghese (p.3) -- Machine Learning and Systems for the Next Frontier in Formal Verification / by Manish Pandey (p.4) -- Verifying Hyperproperties of Hardware Systems / by Bernd Finkbeiner and Markus Rabe (p.5) -- A Paradigm Shift in Verification Methodology / by Pranav Ashar (p.6) -- Program Synthesis for Networks / by Pavol Cern ˇ y´ (p.7) -- The FMCAD 2016 Graduate Student Forum / by Hossein Hojjat (p.8) -- Soundness of the Quasi-Synchronous Abstraction / by Guillaume Baudart, Timothy Bourke and Marc Pouzet (p.9) -- Synthesizing Adaptive Test Strategies from Temporal Logic Specifications / by Roderick Bloem, Robert Koenighofer, Ingo Pill and Franz Roeck (p.17) -- Reducing Interpolant Circuit Size by Ad Hoc Logic Synthesis and SAT-Based Weakening / by Gianpiero Cabodi, Paolo E. Camurati, Marco Palena, Paolo Pasini and Danilo Vendraminetto (p.25) -- Extracting Behaviour from an Executable Instruction Set Model / by Brian Campbell and Ian Stark (p.33) -- Categorical Semantics of Digital Circuits / by Dan Ghica and Achim Jung (p.41) -- Equivalence Checking By Logic Relaxation / by Eugene Goldberg (p.49) -- Minimal unsatisfiable core extraction for SMT / by Ofer Guthmann, Ofer Strichman and Anna Trostanetski (p.57) -- Efficient Uninterpreted Function Abstraction and Refinement for Word-level Model Checking / by Yen-Sheng Ho, Pankaj Chauhan, Pritam Roy, Alan Mishchenko and Robert Brayton (p.65) -- Optimizing Horn Solvers for Network Repair / by Hossein Hojjat, Philipp Ruemmer, Jedidiah McClurg, Pavol Cerny and Nate Foster ˇ (p.73) -- On ∃∀∃! Solving: A Case Study on Automated Synthesis of Magic Card Tricks / by Susmit Jha, Vasumathi Raman and Sanjit A. Seshia (p.81) -- Property-Directed k-Induction / by Dejan Jovanovic and Bruno Dutertre ´ (p.85) -- Lazy Proofs for DPLL(T)-Based SMT Solvers / by Guy Katz, Clark Barrett, Cesare Tinelli, Andrew Reynolds and Liana Hadarean (p.93) -- Verifiable Hierarchical Protocols with Network Invariants on Parametric Systems / by Opeoluwa Matthews, Jesse Bingham and Daniel Sorin (pg.101) -- Modular Specification and Verification of a Cache-Coherent Interface / by Kenneth McMillan (p.109) -- Proof Certificates for SMT-based Model Checkers for Infinite-state Systems / by Alain Mebsout and Cesare Tinelli (p.117) -- Routing under Constraints / by Alexander Nadel (p.125) -- A Consistency Checker for Memory Subsystem Traces / by Matthew Naylor, Simon Moore and Alan Mujumdar (p.133) -- Hybrid Partial Order Reduction with Under-Approximate Dynamic Points-To and Determinacy Information / by Pavel Parizek (p.141) -- Formal Verification of Division and Square Root Implementations, an Oracle Report by / David Rager, Jo Ebergen, Dmitry Nadezhin, Austin Lee, Cuong Chau and Ben Selfridge (p.149) -- Integrating Proxy Theories and Numeric Model Lifting for Floating-Point Arithmetic / by Jaideep Ramachandran and Thomas Wahl (p.153) -- Trustworthy Specifications of ARM v8-A and v8-M System Level Architecture / by Alastair Reid (p.161) -- Equivalence Checking Using Grobner Bases / by Amr Sayed-Ahmed, Daniel Grosse, Mathias Soeken and Rolf Drechsler (p.169) -- Accurate ICP-based Floating-Point Reasoning / by Karsten Scheibler, Felix Neubauer, Ahmed Mahdi, Martin Franzle, Tino Teige, Tom Bienm ¨ uller, Detlef Fehrer and ¨ Bernd Becker (p.177) -- SWAPPER: A Framework for Automatic Generation of Formula Simplifiers based on Conditional Rewrite Rules / by Rohit Singh and Armando Solar-Lezama (p.185) -- Lazy Sequentialization for TSO and PSO via Shared Memory Abstractions / by Ermenegildo Tomasco, Truc Nguyen Lam, Omar Inverso, Bernd Fischer, Salvatore La Torre and Gennaro Parlato (p.193) -- Combining Requirement Mining, Software Model Checking, and Simulation-Based Verification for Industrial Automotive Systems/ by Tomoya Yamaguchi, Tomoyuuki Kaga, Alexandre Donze and Sanjit A Seshia (p.201)
2016-10-01T00:00:00ZProceedings of Formal Methods in Computer-Aided Design, FMCAD 2015Formal Methods in Computer Aided Designhttps://hdl.handle.net/2152/437792019-02-08T20:47:15Z2015-09-01T00:00:00Zdc.title: Proceedings of Formal Methods in Computer-Aided Design, FMCAD 2015
dc.description: Table of Contents: Proving Hybrid Systems / by Andre Platzer (p.1) -- Formal Verification of Arithmetic Datapaths using Algebraic Geometry and Symbolic Computation / by Priyank Kalla (p.2) -- Reactive Synthesis / by Roderick Bloem (p.3) -- Abductive Inference and Its Applications in Program Analysis, Verification, and Synthesis / by Isil Diling (p.4) -- Democratization of Formal Verification with Collective Intelligence / Ziyad Hanna (p.5) -- Detecting Hardware Trojans: A Tale of Two Techniques / by Sharad Malik (p.6) --The Genesis and Development of Model Checking: Fact vs. Fiction / by Allen Emerson (p.7) -- The FMCAD 2015 Graduate Student Forum / by Georg Weissenbacher (p.8) -- Verification of Cache Coherence Protocols wrt. Trace Filters / by Parosh Aziz Abdulla, Mohamed Faouzi Atig, Zeinab Ganjei, Ahmed Rezine and Yunyun Zhu (p.9) -- Compositional Reasoning Gotchas in Practice / by Chirag Agarwal, Paul Hylander, Yogesh Mahajan, Jonathan Michelson and Vigyan Singhal (p.17) -- Universal Boolean Functional Vectors / by Jesse Bingham (p.25) -- Compositional Safety Verification with Max-SMT / by Marc Brockschmidt, Daniel Larraz, Albert Oliveras, Enric Rodr´ıguez Carbonell and Albert Rubio (p.33) --Formal Verification of Automatic Circuit Transformations for Fault-Tolerance by / Dmitry Burlyaev and Pascal Fradet (p.41) -- An SMT-based Approach to Fair Termination Analysis / by Javier Esparza and Philipp J. Meyer (p.49) -- Compositional Recurrence Analysis / by Azadeh Farzan and Zachary Kincaid (p.57) -- Pushing to the Top / by Arie Gurfinkel and Alexander Ivrii (p.65) -- Skolem Functions for Factored Formulas / by Ajith John, Shetal Shah, Supratik Chakraborty, Ashutosh Trivedi and S. Akshay (p.73) -- Theory-Aided Model Checking of Concurrent Transition Systems / by Guy Katz, Clark Barrett and David Harel (p.81) -- Compositional Verification of Procedural Programs using Horn Clauses over Integers and Arrays / by Anvesh Komuravelli, Nikolaj Bjorner, Arie Gurfinkel and Kenneth McMillan (p.89) -- IC3 Software Model Checking on Control Flow Automata / by Tim Lange, Martin R. Neuhaußer and Thomas Noll (p.97) -- Accelerating Invariant Generation / by Kumar Madhukar, Bjorn Wachter, Daniel Kroening, Matt Lewis and Mandayam Srivas (p.105) -- Comparing Different Functional Allocations in Automated Air Traffic Control Design / by Cristian Mattarei, Alessandro Cimatti, Marco Gario, Stefano Tonetta and Kristin Y. Rozier (p.112) -- Pattern-based Synthesis of Synchronization for the C++ Memory Model / by Yuri Meshman, Noam Rinetzky and Eran Yahav (p.120) -- Better Lemmas with Lambda Extraction / by Mathias Preiner, Aina Niemetz and Armin Biere (p.128) -- CAQE: A Certifying QBF Solve / by Markus N. Rabe and Leander Tentrup (p.136) -- Difference Constraints: An adequate Abstraction for Complexity Analysis of Imperative Programs. / by Moritz Sinn, Florian Zuleger and Helmut Veith (p. 144) -- Reverse Engineering with Simulation Graphs / by Mathias Soeken, Baruch Sterin, Rolf Drechsler and Robert Brayton (p.152) -- Template-based Synthesis of Instruction-Level Abstractions for SoC Verification / by Pramod Subramanyan, Yakir Vizel, Sayak Ray and Sharad Malik (p.160) -- Transaction Flows and Executable Models: Formalization and Analysis of Message passing Protocols / by Murali Talupur, Sandip Ray and John Erickson (p.168)
2015-09-01T00:00:00ZProceedings of Formal Methods in Computer-Aided Design, FMCAD 2014Formal Methods in Computer Aided Designhttps://hdl.handle.net/2152/261512019-02-08T20:52:01Z2014-10-01T00:00:00Zdc.title: Proceedings of Formal Methods in Computer-Aided Design, FMCAD 2014
dc.contributor.editor: Claessen, Koen; Kuncak, Viktor
dc.description: Table of Contents: Tutorials -- Challenging Problems in Industrial Formal Verification / by Ziyad Hanna (p. 1) -- Challenges in Bit-Precise Reasoning / by Armin Biere (p. 3) -- Efficient symbolic execution for software testing / by Johannes Kinder (p. 5) -- A Tour of CVC4: How it works, and how to use it / by Morgan Deters, Andrew Reynolds, Tim King, Clark Barrett and Cesare Tinelli (p. 7) -- Invited Talks and Student Forum -- Compiler verification for fun and profit / by Xavier Leroy (p. 9) -- Computer-Aided Verification Technology for Biology / by Thomas A. Henzinger (p. 11) -- Student Forum / by Ruzica Piskac (p. 13) -- Contributed Articles -- Response property checking via distributed state space exploration / by Brad Bingham and Mark Greenstreet (p. 15) -- Towards Pareto-Optimal Parameter Synthesis for Monotonic Cost Functions / by Benjamin Bittner, Marco Bozzano, Alessandro Cimatti, Marco Gario and Alberto Griggio (p. 23) -- SAT-Based Methods for Circuit Synthesis / by Roderick Bloem, Uwe Egly, Patrick Klamp, Robert Könighofer and Florian Lonsing (p. 31) -- Synthesis of Synchronization using Uninterpreted Functions / by Roderick Bloem, Georg Hofferek, Bettina Könighofer, Robert Könighofer, Simon Auβerlechner and Raphael Spörk (p. 35) -- Interpolation with Guided Rfinement: revisiting incrementality in SAT-based Unbounded Model Checking / by Gianpiero Cabodi, Marco Palena and Paolo Pasini (p. 43) -- Efficient Verification of Periodic Programs using Sequential Consistency and Snapshots / by Sagar Chaki, Arie Gurfinkel and Nishant Sinha (p. 51) -- Under-approximate Flowpipes for Non-linear Continuous Systems / by Xin Chen, Sriram Sankaranarayanan and Erika Abraham (p. 59) --Disproving termination with overapproximation / by Byron Cook, Carsten Fuhs, Kaustubh Nimkar and Peter O'Hearn (p. 67) -- Faster Temporal Reasoning for Infinite-State Programs / by Byron Cook, Heidy Khlaaf and Nir Piterman (p. 75) -- Template-based Circuit Understanding / by Adria Gascon, Ashish Tiwari, Bruno Dutertre, Pramod Subramanyan, Sharad Malik and Dejan Jovanovic (p. 83) -- Simulation and Formal Verification of x86 Machine-Code Programs that make System Calls / by Shilpi Goel, Warren Hunt, Matt Kaufmann and Soumava Ghosh (p. 91) -- DRUPing for Interpolants / by Arie Gurfinkel and Yakir Vizel (p. 99) -- Efficient Extraction of Skolem Functions from QRAT Proofs / by Marijn Heule, Martina Seidl and Armin Biere (p. 107) -- Small Inductive Safe Invariants / by Alexander Ivrii, Arie Gurfinkel and Anton Belov (p. 115) -- On Interpolants and Variable Assignments / by Pavel Jancik, Jan Kofron, Simone Fulvio Rollini and Natasha Sharygina (p. 123) -- Post-silicon Timing Diagnosis Made Simple using Formal Technology / by Daher Kaiss and Jonathan Kalechstain (p. 131) -- Leveraging Linear and Mixed Integer Programming for SMT / by Timothy King, Clark Barrett and Cesare Tinelli (p. 139) -- A Program Transformation for Faster Goal-Directed Search / by Akash Lal and Shaz Qadeer (p. 147) -- Infinite-State Backward Exploration of Boolean Broadcast Programs / by Peizun Liu and Thomas Wahl (p. 155) -- Kuai: A Model Checker for Software-defined Networks / by Rupak Majumdar, Sai Deep Tetali and Zilong Wang (p. 163) -- ILP Modulo Data / by Panagiotis Manolios, Vasilis Papavasileiou and Mirek Riedewald (p. 171) -- Turbo-Charging Lemmas on Demand with Don't Care Reasoning / by Aina Niemetz, Mathias Preiner and Armin Biere (p. 179) -- Reduction for Compositional Verification of Multi-Threaded Programs / by Corneliu Popeea, Andrey Rybalchenko and Andreas Wilhelm (p. 187) -- Finding Conflicting Instances of Quantified Formulas in SMT { Andrew Reynolds, Cesare Tinelli and Leonardo De Moura (p. 195) -- Using Interval Constraint Propagation for Pseudo-Boolean Constraint Solving / by Karsten Scheibler and Bernd Becker (p. 203) -- Patient-Specific Models from Inter-Patient Biological Models and Clinical Records / by Enrico Tronci, Toni Mancini, Ivano Salvo, Stefano Sinisi, Federico Mari, Igor Melatti, Annalisa Massini, Francesco Davi, Thomas Dierkes, Rainald Ehrig, Susanna Röblitz, Brigitte Leeners, Tillmann Kruger, Marcel Egli and Fabian Ille (p. 207) --Reducing CTL-live Model Checking to First-Order Logic Validity Checking / by Amirhossein Vakili and Nancy A. Day (p. 215) -- Predicate Abstraction for Reactive Synthesis { Adam Walker and Leonid Ryzhyk (p. 219) -- Author Index (p. 227); 21-24 October, 2014 in Switzerland
2014-10-01T00:00:00Z