


Остановите войну!
for scientists:


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.