Stop the war!
Остановите войну!
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.