Program (with Links) -- Monday -- Friday

Monday, April 24, 2017

08:30 – 09:00
Joost-Pieter Katoen and Parosh Aziz Abdulla
09:00 – 10:00
Invited Talk
Kim G. Larsen
Coherence Spaces and Higher-Order Computation (FOSSACS)
10:30 – 12:30
Coherence Spaces and Uniform Continuity
Kei Matsumoto
(Kyoto University, Japan)
The Free Exponential Modality of Probabilistic Coherence Spaces
Michele Pagani, Raphaëlle Crubillé, Thomas Ehrhard, and Christine Tasson
(University of Paris Diderot, France)
From Qualitative to Quantitative Semantics by Change of Base
James Laird
(University of Bath, UK)
Almost Every Simply Typed Lambda-Term Has a Long Beta-Reduction Sequence
Ryoma Sin'Ya, Kazuyuki Asada, Naoki Kobayashi, and Takeshi Tsukada
(University of Tokyo, Japan)
Information Flow (POST)
10:30 – 12:30
Timing-Sensitive Noninterference through Composition
Willard Rafnsson, Limin Jia, and Lujo Bauer
(MPI-SWS, Germany; Carnegie Mellon University, USA)
Preprint Available Info
Quantifying Vulnerability of Secret Generation using Hyper-distributions
Mário S. Alvim, Piotr Mardziel, and Michael Hicks
(Federal University of Minas Gerais, Brazil; Carnegie Mellon University, USA; University of Maryland at College Park, USA)
Preprint Available Info
A Principled Approach to Tracking Information Flow in the Presence of Libraries
Daniel Hedin, Alexander Sjösten, Frank Piessens, and Andrei Sabelfeld
(Mälardalen University, Sweden; Chalmers University of Technology, Sweden; KU Leuven, Belgium)
Secure Multi-party Computation: Information Flow of Outputs and Game Theory
Patrick Ah-Fat and Michael Huth
(Imperial College London, UK)
Verification Techniques 1 (TACAS)
10:30 – 12:30
An Abstraction Technique for Parameterized Model Checking of Leader Election Protocols: Application to FTSP
Ocan Sankur and Jean-Pierre Talpin
(CNRS, France; Inria, France)
Combining String Abstract Domains for JavaScript Analysis: An Evaluation
Roberto Amadini, Alexander Jordan, Graeme Gange, Francois Gauthier, Peter Schachte, Harald Sondergaard, Peter J. Stuckey, and Chenyi Zhang
(University of Melbourne, Australia; Oracle Labs, Australia; Oracle, Australia; University of Queensland, Australia)
Preprint Available
Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF
Alessandro Cimatti, Alberto Griggio, Ahmed Irfan, Marco Roveri, and Roberto Sebastiani
(Fondazione Bruno Kessler, Italy; University of Trento, Italy)
Bounded Quantifier Instantiation for Checking Inductive Invariants
Yotam M. Y. Feldman, Oded Padon, Neil Immerman, Mooly Sagiv, and Sharon Shoham
(Tel Aviv University, Israel; University of Massachusetts at Amherst, USA)
Algebra and Coalgebra (FOSSACS)
14:00 – 16:00
Algebra, Coalgebra, and Minimization in Polynomial Differential Equations
Michele Boreale
(University of Florence, Italy)
Preprint Available Info
Equational Theories of Abnormal Termination Based on Kleene Algebra
Konstantinos Mamouras
(University of Pennsylvania, USA)
Companions, Codensity, and Causality
Damien Pous and Jurriaan Rot
(CNRS, France; Radboud University Nijmegen, Netherlands)
Preprint Available
Nominal Automata with Name Binding
Lutz Schröder, Dexter Kozen, Stefan Milius, and Thorsten Wißmann
(University of Erlangen-Nuremberg, Germany; Cornell University, USA)
Preprint Available
Security Protocols (POST)
14:00 – 16:00
Automated Verification of Dynamic Root of Trust Protocols
Sergiu Bursuc, Christian Johansen, and Shiwei Xu
(University of Bristol, UK; University of Oslo, Norway; Wuhan Digital and Engineering Institute, China)
Preprint Available
Beyond Subterm-Convergent Equational Theories in Automated Verification of Stateful Protocols
Jannik Dreier, Charles Duménil, Ralf Sasse, and Steve Kremer
(LORIA, France; ETH Zurich, Switzerland)
Preprint Available Info
On Communication Models When Verifying Equivalence Properties
Kushal Babel, Vincent Cheval, and Steve Kremer
(IIT Bombay, India; Inria, France)
Preprint Available Info
SoK: A Survey of Attacks on Ethereum Smart Contracts
Nicola Atzei, Massimo Bartoletti, and Tiziana Cimoli
(University of Cagliari, Italy)
Verification Techniques 2 (TACAS)
14:00 – 16:00
Proving Termination through Conditional Termination
Cristina Borralleras, Marc Brockschmidt, Daniel Larraz, Albert Oliveras, Enric Rodríguez Carbonell, and Albert Rubio
(Universitat de Vic, Spain; Microsoft Research, UK; Universitat Politècnica de Catalunya, Spain)
Preprint Available Info
Efficient Certified Resolution Proof Checking
Luís Cruz-Filipe, Joao Marques-Silva, and Peter Schneider-Kamp
(University of Southern Denmark, Denmark; University of Lisbon, Portugal)
Preprint Available
Precise Widening Operators for Proving Termination by Abstract Interpretation
Nathanaël Courant and Caterina Urban
(ENS, France; ETH Zurich, Switzerland)
Preprint Available
Automatic Verification of Finite Precision Implementations of Linear Controllers
Junkil Park, Miroslav Pajic, Oleg Sokolsky, and Insup Lee
(University of Pennsylvania, USA; Duke University, USA)
16:30 – 18:00
Tutorial 1
Veronique Cortier
Learning (TACAS)
16:30 – 18:00
Learning Symbolic Automata
Samuel Drews and Loris D'Antoni
(University of Wisconsin-Madison, USA)
Preprint Available
ML for ML: Learning Cost Semantics by Experiment
Ankush Das and Jan Hoffmann
(Carnegie Mellon University, USA)
Preprint Available Info
A Novel Learning Algorithm for Buchi Automata Based on Family of DFAs and Classification Trees
Yong Li, Yu-Fang Chen, Lijun Zhang, and Depeng Liu
(Institute of Software at Chinese Academy of Sciences, China; Academia Sinica, Taiwan)
Preprint Available
Tuesday, April 25, 2017
09:00 – 10:00
Invited Talk
Dino Distefano
Games and Automata (FOSSACS)
10:30 – 12:30
On the Existence of Weak Subgame Perfect Equilibria
Véronique Bruyère, Stéphane Le Roux, Arno Pauly, and Jean-Francois Raskin
(University of Mons, Belgium; Université Libre de Bruxelles, Belgium)
Preprint Available
Optimal Reachability in Divergent Weighted Timed Games
Damien Busatto-Gaston, Benjamin Monmege, and Pierre-Alain Reynier
(Aix-Marseille University, France)
Bounding Average-Energy Games
Patricia Bouyer-Decitre, Piotr Hofman, Nicolas Markey, Mickael Randour, and Martin Zimmermann
(CNRS, France; IRISA, France; Université Libre de Bruxelles, Belgium; Saarland University, Germany)
Preprint Available
Logics of Repeating Values on Data Trees and Branching Counter Systems
Sergio Abriola, Diego Figueira, and Santiago Figueira
(University of Buenos Aires, Argentina; CNRS, France)
Security Policies (POST)
10:30 – 12:30
Security Analysis of Cache Replacement Policies
Pablo Canones, Boris Köpf, and Jan Reineke
(IMDEA Software Institute, Spain; Saarland University, Germany)
Preprint Available
Model Checking Exact Cost for Attack Scenarios
Zaruhi Aslanyan and Flemming Nielson
(DTU, Denmark)
Postulates for Revocation Schemes
(University of Luxembourg, Luxembourg)
Preprint Available Info
Defense in Depth Formulation and Usage in Dynamic Access Control
Ridha Khedri, Owain Jones, and Mohammed Alabbad
(McMaster University, Canada; CMC Microsystems, Canada)
Preprint Available
Synthesis 1 (TACAS)
10:30 – 12:30
Hierarchical Network Formation Games
Orna Kupferman and Tami Tamir
(Hebrew University of Jerusalem, Israel; Interdisciplinary Center, Israel)
Synthesis of Recursive ADT Transformers from Reusable Templates
(Massachusetts Institute of Technology, USA; Purdue University, USA; Northeastern University, USA)
Preprint Available
Counterexample-Guided Model Synthesis
Mathias Preiner, Aina Niemetz, and Armin Biere
(JKU Linz, Austria)
Interpolation-Based GR(1) Assumptions Refinement
Davide Giacomo Cavezza and Dalal Alrajeh
(Imperial College London, UK)
Probabilistic Programming (ESOP)
14:00 – 16:00
Commutative Semantics for Probabilistic Programming
(University of Oxford, UK)
Preprint Available
Contextual Equivalence for Probabilistic Programs with Continuous Random Variables and Scoring
Ryan Culpepper and Andrew Cobb
(Northeastern University, USA)
Metric Reasoning about Lambda Terms: The General Case
Raphaëlle Crubillé and Ugo Dal Lago
(ENS Lyon, France; University of Bologna, Italy)
Probabilistic Termination by Monadic Affine Sized Typing
(University of Bologna, Italy; University of Paris Diderot, France)
Preprint Available Info
Automata, Logic, and Formal Languages (FOSSACS)
14:00 – 16:00
Degree of Sequentiality of Weighted Automata
Laure Daviaud, Ismaël Jecker, Pierre-Alain Reynier, and Didier Villevalois
(University of Warsaw, Poland; Université Libre de Bruxelles, Belgium; Aix-Marseille University, France)
Emptiness under Isolation and the Value Problem for Hierarchical Probabilistic Automata
Rohit Chadha, A. Prasad Sistla, and Mahesh Viswanathan
(University of Missouri, USA; University of Illinois at Chicago, USA; University of Illinois at Urbana-Champaign, USA)
Partial Derivatives for Context-Free Languages
Peter Thiemann
(University of Freiburg, Germany)
Dynamic Complexity of the Dyck Reachability
Patricia Bouyer-Decitre and Vincent Jugé
(ENS Cachan, France)
Information Leakage (POST)
14:00 – 16:00
Compositional Synthesis of Leakage Resilient Programs
Arthur Blot, Masaki Yamamoto, and Tachio Terauchi
(ENS Lyon, France; Nagoya University, Japan; JAIST, Japan)
Combining Differential Privacy and Mutual Information for Analyzing Leakages in Workflows
Martin Pettai and Peeter Laud
(Cybernetica, Estonia)
Synthesis 2 (TACAS)
14:00 – 16:00
Connecting Program Synthesis and Reachability: Automatic Program Repair using Test-Input Generation
Thanhvu Nguyen, Westley Weimer, Deepak Kapur, and Stephanie Forrest
(University of Nebraska-Lincoln, USA; University of Virginia, USA; University of New Mexico, USA)
Preprint Available
Scaling Enumerative Program Synthesis via Divide and Conquer
Rajeev Alur, Arjun Radhakrishna, and Abhishek Udupa
(University of Pennsylvania, USA)
Towards Parallel Boolean Functional Synthesis
S. Akshay, Supratik Chakraborty, Ajith John, and Shetal Shah
(IIT Bombay, India; BARC, India)
Encodings of Bounded Synthesis
Peter Faymonville, Bernd Finkbeiner, Leander Tentrup, and Markus N. Rabe
(Saarland University, Germany; University of California at Berkeley, USA)
16:30 – 18:00
Public Lecture
Serge Abibetoul
Wednesday, April 26, 2017
Graph Rewriting (ESOP)
09:00 – 10:00
Confluence of Graph Rewriting with Interfaces
(University of Pisa, Italy; Radboud University Nijmegen, Netherlands; University of Southampton, UK; University College London, UK)
Incremental Update for Graph Rewriting
Pierre Boutillier, Thomas Ehrhard, and Jean Krivine
(Harvard Medical School, USA; IRIF, France; CNRS, France)
Preprint Available
Learning and Inference (FASE)
09:00 – 10:00
Should We Learn Probabilistic Models for Model Checking? A New Approach and an Empirical Study
Jingyi Wang, Jun Sun, Qixia Yuan, and Jun Pang
(Singapore University of Technology and Design, Singapore; University of Luxembourg, Luxembourg)
Preprint Available Info
Bordeaux: A Tool for Thinking Outside the Box
Vajih Montaghami and Derek Rayside
(University of Waterloo, Canada)
Proof Theory (FOSSACS)
09:00 – 10:00
Cyclic Arithmetic Is Equivalent to Peano Arithmetic
Alex Simpson
(University of Ljubljana, Slovenia)
Martin-Lof's Inductive Definitions Are Not Equivalent to Cyclic Proofs
Stefano Berardi and Makoto Tatsuta
(University of Turin, Italy; National Institute of Informatics, Japan)
Tools (TACAS)
09:00 – 10:00
HQSpre: An Effective Preprocessor for QBF and DQBF
Ralf Wimmer, Sven Reimer, Paolo Marin, and Bernd Becker
(University of Freiburg, Germany)
Preprint Available
RPP: Automatic Proof of Relational Properties by Self-Composition (Tool Paper)
Lionel Blatter, Nikolai Kosmatov, Virgile Prevosto, and Pascale Le Gall
(CEA LIST, France; CentraleSupélec, France)
autoCode4: Structural Reactive Synthesis (Tool Paper)
Chih-Hong Cheng, Edward Lee, and Harald Ruess
(fortiss, Germany; University of California at Berkeley, USA)
Concurrency (ESOP)
10:30 – 12:30
Abstract Specifications for Concurrent Maps
(Imperial College London, UK)
Preprint Available Info
Caper: Automatic Verification for Fine-Grained Concurrency
Thomas Dinsdale-Young, Pedro da Rocha Pinto, Kristoffer Just Andersen, and Lars Birkedal
(Aarhus University, Denmark; Imperial College London, UK)
Preprint Available Video
Proving Linearizability using Partial Orders
Artem Khyzha, Mike Dodds, Alexey Gotsman, and Matthew Parkinson
(IMDEA Software Institute, Spain; University of York, UK; Microsoft Research, UK)
Tackling Real-Life Relaxed Concurrency with FSL++
(MPI-SWS, Germany)
Preprint Available Info
Test Selection (FASE)
10:30 – 12:30
Bucketing Failing Tests via Symbolic Analysis
Van-Thuan Pham, Sakaar Khurana, Subhajit Roy, and Abhik Roychoudhury
(National University of Singapore, Singapore; IIT Kanpur, India)
Selective Bisection Debugging
Ripon Saha and Milos Gligoric
(Fujitsu Labs, USA; University of Texas at Austin, USA)
On the Effectiveness of Bug Predictors with Procedural Systems: A Quantitative Study
Cristiano Araújo, Ingrid Nunes, and Daltro José Nunes
(Federal University of Rio Grande do Sul, Brazil)
Preprint Available Info
Probability (FOSSACS)
10:30 – 12:30
On the Relationship between Bisimulation and Trace Equivalence in an Approximate Probabilistic Context
Gaoang Bian and Alessandro Abate
(Google, USA; University of Oxford, UK)
Preprint Available
Computing Continuous Time Markov Chains as Transformers of Unbounded Observation Functions
Tobias Heindel, Vincent Danos, Jakob Grue Simonsen, and Ilias Garnier
(University of Copenhagen, Denmark; CNRS, France; University of Edinburgh, UK)
Preprint Available
Pointless Learning
Florence Clerc, Fredrik Dahlqvist, Vincent Danos, and Ilias Garnier
(McGill University, Canada; University College London, UK; ENS, France; University of Edinburgh, UK)
Preprint Available
On Higher-Order Probabilistic Subrecursion
Flavien Breuvart, Ugo Dal Lago, and Agathe Herrou
(Inria, France; University of Bologna, Italy; ENS Lyon, France)
Preprint Available
Automata (TACAS)
10:30 – 12:30
Lazy Automata Techniques for WS1S
Tomas Fiedor, Lukas Holik, Petr Janku, Ondrej Lengal, and Tomas Vojnar
(Brno University of Technology, Czech Republic)
Preprint Available Info
From LTL and Limit-Deterministic Büchi Automata to Deterministic Parity Automata
Javier Esparza, Jan Kretinsky, Jean-Francois Raskin, and Salomon Sickert
(TU Munich, Germany; Université Libre de Bruxelles, Belgium)
Preprint Available
Index Appearance Record for Transforming Rabin Automata into Parity Automata
Jan Kretinsky, Tobias Meggendorfer, Clara Waldmann, and Maximilian Weininger
(TU Munich, Germany)
Preprint Available
Minimization of Visibly Pushdown Automata using Partial Max-SAT
Christian Schilling, Matthias Heizmann, and Daniel Tischner
(University of Freiburg, Germany)
Language Design (ESOP)
14:00 – 16:00
APLicative Programming with Naperian Functors
(University of Oxford, UK)
Preprint Available Info
Disjoint Polymorphism
João Alpuim, Bruno C. d. S. Oliveira, and Zhiyuan Shi
(University of Hong Kong, China)
Extensible Datasort Refinements
(University of British Columbia, Canada)
The Essence of Functional Programming on Semantic Data
Martin Leinberger, Ralf Lämmel, and Steffen Staab
(University of Koblenz-Landau, Germany; University of Koblenz-Landau, UK)
Concurrency (FOSSACS)
14:00 – 16:00
A Truly Concurrent Game Semantics of the Asynchronous Pi-Calculus
Ken Sakayori and Takeshi Tsukada
(University of Tokyo, Japan)
Local Model Checking in a Logic for True Concurrency
Paolo Baldan and Tommaso Padoan
(University of Padua, Italy)
The Paths to Choreography Extraction
Luís Cruz-Filipe, Kim S. Larsen, and Fabrizio Montesi
(University of Southern Denmark, Denmark)
Preprint Available
On the Undecidability of Asynchronous Session Subtyping
Julien Lange and Nobuko Yoshida
(Imperial College London, UK)
Concurrency and Bisimulation (TACAS)
14:00 – 16:00
CSimpl: A Framework for the Verification of Concurrent Programs using Rely-Guarante
David Sanan, Yang Liu, Zhe Hou, Yongwang Zhao, Fuyuan Zhang, and Alwen Tiu
(Nanyang Technological University, Singapore; Australian National University, Australia; Beihang University, China)
Fair Termination for Parameterized Probabilistic Concurrent Systems
Ondrej Lengal, Anthony Lin, Rupak Majumdar, and Phillip Ruemmer
(Brno University of Technology, Czech Republic; Yale-NUS College, Singapore; MPI-SWS, Germany; Uppsala University, Sweden)
Forward Bisimulations for Nondeterministic Symbolic Finite Automata
(University of Wisconsin, USA; Microsoft Research, USA)
Preprint Available
Up-To Techniques for Weighted Systems
Sebastian Küpper, Barbara König, and Filippo Bonchi
(University of Duisburg-Essen, Germany; ENS Lyon, France)
Verification (ESOP)
16:30 – 18:00
Is Your Software on Dope? Formal Analysis of Surreptitiously Enhanced Programs
Gilles Barthe, Sebastian Biewer, Pedro R. D'Argenio, Bernd Finkbeiner, and Holger Hermanns
(IMDEA Software Institute, Spain; Saarland University, Germany; Universidad Nacional de Córdoba, Germany)
Modular Verification of Procedure Equivalence in the Presence of Memory Allocation
Tim Wood, Shuvendu K. Lahiri, Sophia Drossopoulou, and Susan Eisenbach
(Imperial College London, UK; Microsoft Research, USA)
Verifying Robustness of Event-Driven Asynchronous Programs against Concurrency
Ahmed Bouajjani, Michael Emmi, Constantin Enea, Burcu Kulahcioglu Ozkan, and Serdar Tasiran
(University of Paris Diderot, France; Nokia Bell Labs, USA; Koç University, Turkey)
Lambda Calculus and Constructive Proof (FOSSACS)
16:30 – 18:00
A Lambda-Free Higher-Order Recursive Path Order
Jasmin Christian Blanchette, Uwe Waldmann, and Daniel Wand
(Inria, France; Max Planck Institute for Informatics, Germany)
Preprint Available
Automated Constructivization of Proofs
Frederic Gilbert
(École des Ponts ParisTech, France)
Hybrid Systems (TACAS)
16:30 – 18:00
Rigorous Simulation-Based Analysis of Linear Hybrid Systems
Stanley Bak and Parasara Sridhar Duggirala
(Air Force Research Lab, USA; University of Connecticut, USA)
Preprint Available Video
HARE: A Hybrid Abstraction Refinement Engine for Verifying Non-linear Hybrid Automata
Nima Roohi, Pavithra Prabhakar, and Mahesh Viswanathan
(University of Illinois at Urbana-Champaign, USA; Kansas State University, USA)
Counterexample-Guided Refinement of Template Polyhedra
Sergiy Bogomolov, Goran Frehse, Mirco Giacobbe, and Thomas Henzinger
(Australian National University, Australia; University of Grenoble, France; IST Austria, Austria)
Thursday, April 27, 2017
09:00 – 10:00
Invited Talk
Michael Ernst
Automated Verification (ESOP)
10:30 – 12:30
Conditional Dyck-CFL Reachability Analysis for Complete and Efficient Library Summarization
Hao Tang, Di Wang, Yingfei Xiong, Lingming Zhang, Xiaoyin Wang, and Lu Zhang
(Peking University, China; University of Texas at Dallas, USA; University of Texas at San Antonio, USA)
Preprint Available Info
Faster Algorithms for Weighted Recursive State Machines
Krishnendu Chatterjee, Bernhard Kragl, Samarth Mishra, and Andreas Pavlogiannis
(IST Austria, Austria; IIT Bombay, India)
Preprint Available
ML and Extended BVASS
Conrad Cotton-Barratt, Andrzej Murawski, and C.-H. Luke Ong
(University of Oxford, UK; University of Warwick, UK)
Modular Verification of Higher-Order Functional Programs
(University of Tokyo, Japan)
Program and System Analysis (FASE)
10:30 – 12:30
Inference and Evolution of TypeScript Declaration Files
Erik Krogh Kristensen and Anders Møller
(Aarhus University, Denmark)
Preprint Available Info
Explicit Connection Actions in Multiparty Session Types
Raymond Hu and Nobuko Yoshida
(Imperial College London, UK)
Change and Delay Contracts for Hybrid System Component Verification
Andreas Müller, Stefan Mitsch, Werner Retschitzegger, Wieland Schwinger, and André Platzer
(JKU Linz, Austria; Carnegie Mellon University, USA)
Preprint Available Info
Precise Version Control of Trees with Line-Based Version Control Systems
Dimitar Asenov, Balz Guenat, Peter Müller, and Martin Otth
(ETH Zurich, Switzerland; Ergon Informatik, Switzerland)
Preprint Available Video Info
Semantics and Category Theory (FOSSACS)
10:30 – 12:30
A Light Modality for Recursion
(University of Leicester, UK)
Preprint Available
Unifying Guarded and Unguarded Iteration
Sergey Goncharov, Lutz Schröder, Christoph Rauch, and Maciej Piróg
(University of Erlangen-Nuremberg, Germany; KU Leuven, Belgium)
Preprint Available
Partiality, Revisited: The Partiality Monad as a Quotient Inductive-Inductive Type
Thorsten Altenkirch, Nils Anders Danielsson, and Nicolai Kraus
(University of Nottingham, UK; University of Gothenburg, Sweden)
On the Semantics of Intensionality
(University of Oxford, UK)
Preprint Available
Security (TACAS)
10:30 – 12:30
Static Detection of DoS Vulnerabilities in Programs That Use Regular Expressions
Valentin Wuestholz, Oswaldo Olivo, Marijn Heule, and Isil Dillig
(University of Texas at Austin, USA)
Discriminating Traces with Time
Saeid Tizpaz-Niari, Pavol Cerny, Bor-Yuh Evan Chang, Sriram Sankaranarayanan, and Ashutosh Trivedi
(University of Colorado at Boulder, USA)
Directed Automated Memory Performance Testing
Sudipta Chattopadhyay
(Saarland University, Germany)
Context-Bounded Analysis for POWER
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, and Tuan Phong Ngo
(Uppsala University, Sweden; University of Paris Diderot, France)
Theorem Proving (ESOP)
14:00 – 16:00
Comprehending Isabelle/HOL's Consistency
Ondřej Kunčar and Andrei Popescu
(TU Munich, Germany)
Friends with Benefits: Implementing Corecursion in Foundational Proof Assistants
(Inria, Germany; École Polytechnique, France; ETH Zurich, Switzerland; Middlesex University, UK)
Preprint Available Info
Generalizing Inference Systems by Coaxioms
Davide Ancona, Francesco Dagnino, and Elena Zucca
(University of Genoa, Italy)
Preprint Available Info
Verified Characteristic Formulae for CakeML
Armaël Guéneau, Magnus O. Myreen, Ramana Kumar, and Michael Norrish
(ENS Lyon, France; Chalmers University of Technology, Sweden; Data61 at CSIRO, Australia)
Graph Modelling and Transformation (FASE)
14:00 – 16:00
StaticGen: Static Generation of UML Sequence Diagrams
Christopher Alvin, Supratik Mukhopadhyay, and Brian Peterson
(Bradley University, USA; Louisiana State University, USA)
Inter-model Consistency Checking using Triple Graph Grammars and Linear Optimization Techniques
Erhan Leblebici, Anthony Anjorin, and Andy Schürr
(TU Darmstadt, Germany; University of Paderborn, Germany)
GTS Families for the Flexible Composition of Graph Transformation Systems
Steffen Zschaler and Francisco Durán
(King's College London, UK; University of Málaga, Spain)
Symbolic Model Generation for Graph Properties
Sven Schneider, Leen Lambers, and Fernando Orejas
(HPI, Germany; Universitat Politècnica de Catalunya, Spain)
Competition on Software Verification (SV-COMP) (TACAS)
14:00 – 16:00
Competition on Software Verification (Competition Report)
(LMU Munich, Germany)
AProVE: Proving and Disproving Termination of Memory-Manipulating C Programs (Competition Contribution)
Jera Hensel, Frank Emrich, Florian Frohn, Thomas Stroeder, and Jürgen Giesl
(RWTH Aachen University, Germany)
Preprint Available
CPA-BAM-BnB: Block-Abstraction Memoization and Region-Based Memory Models for Predicate Abstractions (Competition Contribution)
Pavel Andrianov, Vadim Mutilin, Karlheinz Friedberger, Mikhail Mandrykin, and Anton Volkov
(ISP RAS, Russia; University of Passau, Germany)
DepthK: A k-Induction Verifier Based on Invariant Inference for C Programs (Competition Contribution)
Williame Rocha, Herbert O. Rocha, Hussama Ismail, Lucas Cordeiro, and Bernd Fischer
(Federal University of Amazonas, Brazil; Federal University of Roraima, Brazil; University of Oxford, UK; Stellenbosch University, South Africa)
Preprint Available
Forester: From Heap Shapes to Automata Predicates (Competition Contribution)
Martin Hruska, Lukas Holik, Tomas Vojnar, Ondrej Lengal, Adam Rogalewicz, and Jiri Simacek
(Brno University of Technology, Czech Republic)
Preprint Available Info
HipTNT+: A Termination and Non-termination Analyzer by Second-Order Abduction (Competition Contribution)
Ton Chanh Le, Quang-Trung Ta, and Wei-Ngan Chin
(National University of Singapore, Singapore)
Lazy-CSeq 2.0: Combining Lazy Sequentialization with Abstract Interpretation (Competition Contribution)
Truc Nguyen Lam, Omar Inverso, Bernd Fischer, Salvatore La Torre, and Gennaro Parlato
(University of Southampton, UK; Stellenbosch University, South Africa; University of Salerno, Italy)
Skink 2.0: Static Analysis of LLVM Intermediate Representation (Competition Contribution)
Franck Cassez, Tony Sloane, Matt Roberts, Matthew Pigram, Pablo González De Aledo, and Pongsak Suvanpong
(Macquarie University, Australia; University of Cantabria, Spain)
Symbiotic 4: Beyond Reachability (Competition Contribution)
Marek Chalupa, Martina Vitovská, Martin Jonáš, Jiri Slaby, and Jan Strejcek
(Masaryk University, Czech Republic)
Preprint Available
Optimizing and Caching SMT Queries in SymDIVINE (Competition Contribution)
Martin Jonáš, Jan Mrázek, Vladimír Štill, Jiří Barnat, and Henrich Lauko
(Masaryk University, Czech Republic)
VeriAbs: Verification by Abstraction (Competition Contribution)
Bharti Chimdyalwar, Priyanka Darke, Avriti Chauhan, Punit Shah, Shrawan Kumar, and Venkatesh R
(Tata Consultancy Services, India)
Ultimate Automizer with an On-Demand Construction of Floyd-Hoare Automata (Competition Contribution)
Matthias Heizmann, Yu-Wen Chen, Daniel Dietsch, Marius Greitschus, Betim Musa, Alexander Nutz, Claus Schätzle, Christian Schilling, Frank Schüssele, and Andreas Podelski
(University of Freiburg, Germany)
Ultimate Taipan: Trace Abstraction and Abstract Interpretation (Competition Contribution)
Marius Greitschus, Daniel Dietsch, Matthias Heizmann, Alexander Nutz, Claus Schätzle, Christian Schilling, Frank Schüssele, and Andreas Podelski
(University of Freiburg, Germany)
16:30 – 18:00
Ken McMillan
Run-Time Verification and Logic (TACAS)
16:30 – 18:00
Rewriting-Based Runtime Verification of Alternation-Free HyperLTL Formulas
Noel Brett, Umair Siddique, and Borzoo Bonakdarpour
(McMaster University, Canada)
Almost Event-Rate Independent Monitoring of Metric Temporal Logic
David Basin, Bhargav Bhatt, and Dmitriy Traytel
(ETH Zurich, Switzerland)
Preprint Available
Optimal Translation of LTL to Limit Deterministic Automata
Dileep Kini and Mahesh Viswanathan
(University of Illinois at Urbana-Champaign, USA)
Preprint Available Info
Friday, April 28, 2017
09:00 – 10:00
Invited Talk
Joel Ouaknine
Separation Logic (ESOP)
10:30 – 12:30
A Higher-Order Logic for Concurrent Termination-Preserving Refinement
Joseph Tassarotti, Ralf Jung, and Robert Harper
(Carnegie Mellon University, USA; MPI-SWS, Germany)
Temporary Read-Only Permissions for Separation Logic
(Inria, France)
Preprint Available Info
The Essence of Higher-Order Concurrent Separation Logic
Robbert Krebbers, Ralf Jung, Aleš Bizjak, Jacques-Henri Jourdan, Derek Dreyer, and Lars Birkedal
(Delft University of Technology, Netherlands; MPI-SWS, Germany; Aarhus University, Denmark)
Preprint Available
Unified Reasoning about Robustness Properties of Symbolic-Heap Separation Logic
Christina Jansen, Jens Katelaan, Christoph Matheja, Thomas Noll, and Florian Zuleger
(RWTH Aachen University, Germany; Vienna University of Technology, Austria)
Model Transformations (FASE)
10:30 – 12:30
Traceability Mappings as a Fundamental Instrument in Model Transformations
Zinovy Diskin, Abel Gómez-Llana, and Jordi Cabot
(McMaster University, Canada; Open University of Catalonia, Spain; ICREA, Spain)
Preprint Available
Reusing Model Transformations through Typing Requirement Models
Juan De Lara, Juri Di Rocco, Davide Di Ruscio, Esther Guerra, Ludovico Iovino, Alfonso Pierantonio, and Jesús Sánchez Cuadrado
(Autonomous University of Madrid, Spain; University of L'Aquila, Italy; Gran Sasso Science Institute, Italy)
Preprint Available
Change-Preserving Model Repair
Gabriele Taentzer, Manuel Ohrndorf, Yngve Lamo, and Adrian Rutle
(University of Marburg, Germany; University of Siegen, Germany; Western Norway University of Applied Sciences, Norway)
A Deductive Approach for Fault Localization in ATL Model Transformations
Zheng Cheng and Massimo Tisi
(AtlanMod, France)
Quantitative Systems 1 (TACAS)
10:30 – 12:30
Sequential Convex Programming for the Efficient Verification of Parametric MDPs
Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, Ivan Papusha, Hasan A. Poonawala, and Ufuk Topcu
(University of Texas at Austin, USA; RWTH Aachen University, Germany)
Preprint Available
JANI: Quantitative Model and Tool Interaction
Carlos E. Budde, Christian Dehnert, Ernst Moritz Hahn, Arnd Hartmanns, Sebastian Junges, and Andrea Turrini
(Universidad Nacional de Córdoba, Argentina; RWTH Aachen University, Germany; Institute of Software at Chinese Academy of Sciences, China; University of Twente, Netherlands)
Computing Scores of Forwarding Schemes in Switched Networks with Probabilistic Faults
Guy Avni, Shubham Goel, Thomas Henzinger, and Guillermo Rodriguez-Navas
(IST Austria, Austria; IIT Bombay, India; Mälardalen University, Sweden)
Preprint Available
Long-Run Rewards for Markov Automata
Yuliya Butkova, Holger Hermanns, and Ralf Wimmer
(Saarland University, Germany; University of Freiburg, Germany)
Session Types (ESOP)
14:00 – 16:00
Context-Free Session Type Inference
(University of Turin, Italy)
Preprint Available Info
Linearity, Control Effects, and Behavioural Types
Luis Caires and Jorge A. Pérez
(Nova University of Lisbon, Portugal; University of Groningen, Netherlands)
Observed Communication Semantics for Classical Processes
Robert Atkey
(University of Strathclyde, UK)
The Power of Non-determinism in Higher-Order Implicit Complexity
Cynthia Kop and Jakob Grue Simonsen
(University of Copenhagen, Denmark)
Preprint Available
Configuration and Synthesis (FASE)
14:00 – 16:00
OpenSAW: Open Security Analysis Workbench
Noomene Ben Henda, Björn Johansson, Patrik Lantz, Karl Norrman, Pasi Saarinen, and Oskar Segersvärd
(Ericsson Research, Sweden; KTH, Sweden)
Visual Configuration of Mobile Privacy Policies
Abdulbaki Aydin, David Piorkowski, Omer Tripp, Pietro Ferrara, and Marco Pistoia
(University of California at Santa Barbara, USA; IBM Research, USA; Google, USA; Julia, Italy)
Automated Workarounds from Java Program Specifications Based on SAT Solving
Marcelo Ariel Uva, Pablo Ponzio, Germán Regis, Nazareno Aguirre, and Marcelo F. Frias
(Universidad Nacional de Río Cuarto, Argentina; Buenos Aires Institute of Technology, Argentina)
Preprint Available Info
Slicing from Formal Sematics: Chisel
Adrian Riesco, Irina Mariuca Asavoae, and Mihail Asavoae
(Complutense University of Madrid, Spain; Inria, France)
Preprint Available Info
EasyInterface: A Toolkit for Rapid Development of GUIs for Research Prototype Tools
Jesus Doménech, Samir Genaim, Einar Broch Johnsen, and Rudolf Schlatte
(Complutense University of Madrid, Spain; University of Oslo, Norway)
Preprint Available Video Info
14:00 – 16:00
HiFrog: SMT-Based Function Summarization for Software Verification
Leonardo Alt, Sepideh Asadi, Hana Chockler, Karine Even Mendoza, Grigory Fedyukovich, Antti Hyvärinen, and Natasha Sharygina
(University of Lugano, Switzerland; King's College London, UK; University of Washington, USA)
Congruence Closure with Free Variables
Haniel Barbosa, Pascal Fontaine, and Andrew Reynolds
(LORIA, France; University of Iowa, USA)
On Optimization Modulo Theories, MaxSMT, and Sorting Networks
Roberto Sebastiani and Patrick Trentin
(University of Trento, Italy)
The Automatic Detection of Token Structures and Invariants using SAT Checking
Pedro Antonino, Thomas Gibson-Robinson, and Bill Roscoe
(Federal University of Pernambuco, Brazil; University of Oxford, UK)
Type Theory (ESOP)
16:30 – 18:00
A Classical Sequent Calculus with Dependent Types
Étienne Miquey
(Inria, Uruguay)
Lincx: A Linear Logical Framework with First-Class Context
Aina L. Georges, Agata Murawska, Shawn Otis, and Brigitte Pientka
(McGill University, Canada; IT University of Copenhagen, Denmark)
Programs using Syntax with First-Class Binders
Francisco Ferreira and Brigitte Pientka
(McGill University, Canada)
Software Product Lines (FASE)
16:30 – 18:00
Family-Based Model Checking with mCRL2
Maurice H. ter Beek, Erik De Vink, and Tim Willemse
(ISTI-CNR, Italy; Eindhoven University of Technology, Netherlands)
Variability-Specific Abstraction Refinement for Family-Based Model Checking
(IT University of Copenhagen, Denmark)
Preprint Available
A Unified and Formal Programming Model for Deltas and Traits
Ferruccio Damiani, Reiner Hähnle, Eduard Kamburjan, and Michael Lienhardt
(University of Turin, Italy; TU Darmstadt, Germany)
Quantitative Systems 2 (TACAS)
16:30 – 18:00
Maximizing the Conditional Expected Reward for Reaching the Goal
Christel Baier, Joachim Klein, Sascha Klüppelholz, and Sascha Wunderlich
(TU Dresden, Germany)
ARES: Adaptive Receding-Horizon Synthesis of Optimal Plans
Anna Lukina, Lukas Esterle, Christian Hirsch, Ezio Bartocci, Junxing Yang, Ashish Tiwari, Scott A. Smolka, and Radu Grosu
(Vienna University of Technology, Austria; Stony Brook University, USA; SRI International, USA)
Preprint Available
FlyFast: A Mean Field Model Checker (Tool Paper)
Diego Latella, Michele Loreti, and Mieke Massink
(ISTI-CNR, Italy; University of Florence, Italy)
ERODE: A Tool for the Evaluation and Reduction of Ordinary Differential Equations (Tool Paper)
(Microsoft Research, UK; IMT School for Advanced Studies Lucca, Italy)
Preprint Available

Who's online

We have 113 guests and no members online

Site Hosted by