


default search action
23rd TACAS 2017: Uppsala, Sweden (Part of ETAPS 2017)
- Axel Legay, Tiziana Margaria:

Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part I. Lecture Notes in Computer Science 10205, 2017, ISBN 978-3-662-54576-8
Invited Talk
- Kim Guldstrand Larsen

:
Validation, Synthesis and Optimization for Cyber-Physical Systems. 3-20
Verification Techniques I
- Ocan Sankur, Jean-Pierre Talpin:

An Abstraction Technique for Parameterized Model Checking of Leader Election Protocols: Application to FTSP. 23-40 - Roberto Amadini, Alexander Jordan

, Graeme Gange
, François Gauthier, Peter Schachte
, Harald Søndergaard
, Peter J. Stuckey, Chenyi Zhang
:
Combining String Abstract Domains for JavaScript Analysis: An Evaluation. 41-57 - Alessandro Cimatti

, Alberto Griggio
, Ahmed Irfan
, Marco Roveri
, Roberto Sebastiani:
Invariant Checking of NRA Transition Systems via Incremental Reduction to LRA with EUF. 58-75 - Yotam M. Y. Feldman

, Oded Padon, Neil Immerman, Mooly Sagiv, Sharon Shoham
:
Bounded Quantifier Instantiation for Checking Inductive Invariants. 76-95
Verification Techniques II
- Cristina Borralleras

, Marc Brockschmidt, Daniel Larraz
, Albert Oliveras, Enric Rodríguez-Carbonell
, Albert Rubio
:
Proving Termination Through Conditional Termination. 99-117 - Luís Cruz-Filipe

, João Marques-Silva, Peter Schneider-Kamp
:
Efficient Certified Resolution Proof Checking. 118-135 - Nathanaël Courant

, Caterina Urban:
Precise Widening Operators for Proving Termination by Abstract Interpretation. 136-152 - Junkil Park, Miroslav Pajic

, Oleg Sokolsky
, Insup Lee:
Automatic Verification of Finite Precision Implementations of Linear Controllers. 153-169
Learning
- Samuel Drews, Loris D'Antoni:

Learning Symbolic Automata. 173-189 - Ankush Das

, Jan Hoffmann:
ML for ML: Learning Cost Semantics by Experiment. 190-207 - Yong Li

, Yu-Fang Chen
, Lijun Zhang, Depeng Liu
:
A Novel Learning Algorithm for Büchi Automata Based on Family of DFAs and Classification Trees. 208-226
Synthesis I
- Orna Kupferman, Tami Tamir:

Hierarchical Network Formation Games. 229-246 - Jeevana Priya Inala, Nadia Polikarpova, Xiaokang Qiu

, Benjamin S. Lerner, Armando Solar-Lezama:
Synthesis of Recursive ADT Transformations from Reusable Templates. 247-263 - Mathias Preiner

, Aina Niemetz
, Armin Biere
:
Counterexample-Guided Model Synthesis. 264-280 - Davide G. Cavezza, Dalal Alrajeh:

Interpolation-Based GR(1) Assumptions Refinement. 281-297
Synthesis II
- ThanhVu Nguyen, Westley Weimer, Deepak Kapur, Stephanie Forrest

:
Connecting Program Synthesis and Reachability: Automatic Program Repair Using Test-Input Generation. 301-318 - Rajeev Alur, Arjun Radhakrishna, Abhishek Udupa:

Scaling Enumerative Program Synthesis via Divide and Conquer. 319-336 - S. Akshay, Supratik Chakraborty

, Ajith K. John, Shetal Shah:
Towards Parallel Boolean Functional Synthesis. 337-353 - Peter Faymonville

, Bernd Finkbeiner, Markus N. Rabe, Leander Tentrup:
Encodings of Bounded Synthesis. 354-370
Tools
- Ralf Wimmer

, Sven Reimer, Paolo Marin, Bernd Becker
:
HQSpre - An Effective Preprocessor for QBF and DQBF. 373-390 - Lionel Blatter, Nikolai Kosmatov

, Pascale Le Gall
, Virgile Prevosto
:
RPP: Automatic Proof of Relational Properties by Self-composition. 391-397 - Chih-Hong Cheng, Edward A. Lee, Harald Ruess:

autoCode4: Structural Controller Synthesis. 398-404
Automata
- Tomás Fiedor, Lukás Holík

, Petr Janku, Ondrej Lengál
, Tomás Vojnar
:
Lazy Automata Techniques for WS1S. 407-425 - Javier Esparza

, Jan Kretínský, Jean-François Raskin
, Salomon Sickert:
From LTL and Limit-Deterministic Büchi Automata to Deterministic Parity Automata. 426-442 - Jan Kretínský, Tobias Meggendorfer

, Clara Waldmann
, Maximilian Weininger
:
Index Appearance Record for Transforming Rabin Automata into Parity Automata. 443-460 - Matthias Heizmann

, Christian Schilling
, Daniel Tischner:
Minimization of Visibly Pushdown Automata Using Partial Max-SAT. 461-478
Concurrency and Bisimulation
- David Sanán

, Yongwang Zhao, Zhe Hou
, Fuyuan Zhang, Alwen Tiu, Yang Liu
:
CSimpl: A Rely-Guarantee-Based Framework for Verifying Concurrent Programs. 481-498 - Ondrej Lengál

, Anthony Widjaja Lin
, Rupak Majumdar, Philipp Rümmer:
Fair Termination for Parameterized Probabilistic Concurrent Systems. 499-517 - Loris D'Antoni, Margus Veanes:

Forward Bisimulations for Nondeterministic Symbolic Finite Automata. 518-534 - Filippo Bonchi

, Barbara König, Sebastian Küpper:
Up-To Techniques for Weighted Systems. 535-552
Hybrid Systems
- Stanley Bak, Parasara Sridhar Duggirala:

Rigorous Simulation-Based Analysis of Linear Hybrid Systems. 555-572 - Nima Roohi, Pavithra Prabhakar, Mahesh Viswanathan:

HARE: A Hybrid Abstraction Refinement Engine for Verifying Non-linear Hybrid Automata. 573-588 - Sergiy Bogomolov

, Goran Frehse
, Mirco Giacobbe
, Thomas A. Henzinger:
Counterexample-Guided Refinement of Template Polyhedra. 589-606

manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.


Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCID














