Membership-based synthesis of linear hybrid automata
M. Garcia Soto, T.A. Henzinger, C. Schilling, L. Zeleznik, in:, 31st International Conference on Computer-Aided Verification, Springer, 2019, pp. 297–314.
LibreCat: https://research-explorer.ista.ac.at/record/6493
DOI: 10.1007/978-3-030-25540-4_16
WoS: 000491468000016

Infinite-duration bidding games
G. Avni, T.A. Henzinger, V.K. Chonev, Journal of the ACM 66 (2019).
LibreCat: https://research-explorer.ista.ac.at/record/6752
DOI: 10.1145/3340295
WoS: 000487714900008
arXiv: 1705.01433

From real-time logic to timed automata
T. Ferrere, O. Maler, D. Nidkovi, A. Pnueli, Journal of the ACM 66 (2019).
LibreCat: https://research-explorer.ista.ac.at/record/7109
DOI: 10.1145/3286976
WoS: 000495406300005

Transient memory in gene regulation
C.C. Guet, T.A. Henzinger, C. Igler, T. Petrov, A. Sezgin, in:, 17th International Conference on Computational Methods in Systems Biology, Springer Nature, 2019, pp. 155–187.
LibreCat: https://research-explorer.ista.ac.at/record/7147
DOI: 10.1007/978-3-030-31304-3_9
WoS: 000557875100009

Shape expressions for specifying and extracting signal features
D. Nidkovi, X. Qin, T. Ferrere, C. Mateis, J. Deshmukh, in:, 19th International Conference on Runtime Verification, Springer Nature, 2019, pp. 292–309.
LibreCat: https://research-explorer.ista.ac.at/record/7159
DOI: 10.1007/978-3-030-32079-9_17
WoS: 000570006300017

Piecewise robust barrier tubes for nonlinear hybrid systems with uncertainty
H. Kong, E. Bartocci, Y. Jiang, T.A. Henzinger, in:, 17th International Conference on Formal Modeling and Analysis of Timed Systems, Springer Nature, 2019, pp. 123–141.
LibreCat: https://research-explorer.ista.ac.at/record/7231
DOI: 10.1007/978-3-030-29662-9_8
WoS: 000611677700008
arXiv: 1907.11514

Mixed-time signal temporal logic
T. Ferrere, O. Maler, D. Nickovic, in:, 17th International Conference on Formal Modeling and Analysis of Timed Systems, Springer Nature, 2019, pp. 59–75.
LibreCat: https://research-explorer.ista.ac.at/record/7232
DOI: 10.1007/978-3-030-29662-9_4
WoS: 000611677700004

Automatic time-unbounded reachability analysis of hybrid systems
M. Giacobbe, Automatic Time-Unbounded Reachability Analysis of Hybrid Systems, Institute of Science and Technology Austria, 2019.
LibreCat: https://research-explorer.ista.ac.at/record/6894
DOI: 10.15479/AT:ISTA:6894

Handbook of Model Checking
E.M. Clarke, T.A. Henzinger, H. Veith, R. Bloem, Handbook of Model Checking, 1st ed., Springer Nature, Cham, 2018.
LibreCat: https://research-explorer.ista.ac.at/record/3300
DOI: 10.1007/978-3-319-10575-8

Introduction to model checking
E. Clarke, T.A. Henzinger, H. Veith, in:, T.A. Henzinger (Ed.), Handbook of Model Checking, Springer, 2018, pp. 1–26.
LibreCat: https://research-explorer.ista.ac.at/record/60
DOI: 10.1007/978-3-319-10575-8_1

Computing average response time
K. Chatterjee, T.A. Henzinger, J. Otop, in:, M. Lohstroh, P. Derler, M. Sirjani (Eds.), Principles of Modeling, Springer, 2018, pp. 143–161.
LibreCat: https://research-explorer.ista.ac.at/record/86
DOI: 10.1007/978-3-319-95246-8_9

Timed network games with clocks
G. Avni, S. Guha, O. Kupferman, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018.
LibreCat: https://research-explorer.ista.ac.at/record/6005
DOI: 10.4230/LIPICS.MFCS.2018.23

Synchronizing the asynchronous
B. Kragl, S. Qadeer, T.A. Henzinger, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018.
LibreCat: https://research-explorer.ista.ac.at/record/133
DOI: 10.4230/LIPIcs.CONCUR.2018.21

AMT 2.0: Qualitative and quantitative trace analysis with extended signal temporal logic
D. Nickovic, O. Lebeltel, O. Maler, T. Ferrere, D. Ulus, in:, D. Beyer, M. Huisman (Eds.), Springer, 2018, pp. 303–319.
LibreCat: https://research-explorer.ista.ac.at/record/299
DOI: 10.1007/978-3-319-89963-3_18
WoS: 00445822600018

A theory of register monitors
T. Ferrere, T.A. Henzinger, E. Saraç, in:, IEEE, 2018, pp. 394–403.
LibreCat: https://research-explorer.ista.ac.at/record/144
DOI: 10.1145/3209108.3209194
WoS: 000545262800041

Efficient parametric identification for STL
A. Bakhirkin, T. Ferrere, O. Maler, in:, Proceedings of the 21st International Conference on Hybrid Systems, ACM, 2018, pp. 177–186.
LibreCat: https://research-explorer.ista.ac.at/record/182
DOI: 10.1145/3178126.3178132
WoS: 000474781600020

Infinite-duration poorman-bidding games
G. Avni, T.A. Henzinger, R. Ibsen-Jensen, in:, Springer, 2018, pp. 21–36.
LibreCat: https://research-explorer.ista.ac.at/record/5788
DOI: 10.1007/978-3-030-04612-5_2
WoS: 000865933000002
arXiv: 1804.04372

Layered Concurrent Programs
B. Kragl, S. Qadeer, in:, Springer, 2018, pp. 79–102.
LibreCat: https://research-explorer.ista.ac.at/record/160
DOI: 10.1007/978-3-319-96145-3_5
WoS: 000491481600005

Localizing faults in simulink/stateflow models with STL
E. Bartocci, T. Ferrere, N. Manjunath, D. Nickovic, in:, Association for Computing Machinery, Inc, 2018, pp. 197–206.
LibreCat: https://research-explorer.ista.ac.at/record/183
DOI: 10.1145/3178126.3178131
WoS: 000474781600022

Monitoring temporal logic with clock variables
A. Elgyütt, T. Ferrere, T.A. Henzinger, in:, Springer, 2018, pp. 53–70.
LibreCat: https://research-explorer.ista.ac.at/record/81
DOI: 10.1007/978-3-030-00151-3_4
WoS: 000884993200004

Online timed pattern matching using automata
A. Bakhirkin, T. Ferrere, D. Nickovic, O. Maler, E. Asarin, in:, Springer, 2018, pp. 215–232.
LibreCat: https://research-explorer.ista.ac.at/record/78
DOI: 10.1007/978-3-030-00151-3_13
WoS: 000884993200013

Parameter-independent strategies for pMDPs via POMDPs
S. Arming, E. Bartocci, K. Chatterjee, J.P. Katoen, A. Sokolova, in:, Springer, 2018, pp. 53–70.
LibreCat: https://research-explorer.ista.ac.at/record/79
DOI: 10.1007/978-3-319-99154-2_4
WoS: 000548912200004
arXiv: 1806.05126

Reachable set over-approximation for nonlinear systems using piecewise barrier tubes
H. Kong, E. Bartocci, T.A. Henzinger, in:, Springer, 2018, pp. 449–467.
LibreCat: https://research-explorer.ista.ac.at/record/142
DOI: 10.1007/978-3-319-96145-3_24
WoS: 000491481600024

Safety-assured model-driven design of the multifunction vehicle bus controller
Y. Jiang, H. Liu, H. Song, H. Kong, R. Wang, Y. Guan, L. Sha, IEEE Transactions on Intelligent Transportation Systems 19 (2018) 3320–3333.
LibreCat: https://research-explorer.ista.ac.at/record/434
DOI: 10.1109/TITS.2017.2778077
WoS: 000446651100020

Space-time interpolants
G. Frehse, M. Giacobbe, T.A. Henzinger, in:, Springer, 2018, pp. 468–486.
LibreCat: https://research-explorer.ista.ac.at/record/140
DOI: 10.1007/978-3-319-96145-3_25
WoS: 000491481600025

Strategy representation by decision trees in reactive synthesis
T. Brázdil, K. Chatterjee, J. Kretinsky, V. Toman, in:, Springer, 2018, pp. 385–407.
LibreCat: https://research-explorer.ista.ac.at/record/297
DOI: 10.1007/978-3-319-89960-2_21
WoS: 000546326300021

Synthesis from component libraries with costs
G. Avni, O. Kupferman, Theoretical Computer Science 712 (2018) 50–72.
LibreCat: https://research-explorer.ista.ac.at/record/608
DOI: 10.1016/j.tcs.2017.11.001
WoS: 000424959200003

The compound interest in relaxing punctuality
T. Ferrere, in:, Springer, 2018, pp. 147–164.
LibreCat: https://research-explorer.ista.ac.at/record/156
DOI: 10.1007/978-3-319-95582-7_9
WoS: 000489765800009

Keynote: The first-order logic of signals
A. Bakhirkin, T. Ferrere, T.A. Henzinger, D. Nickovicl, in:, 2018 International Conference on Embedded Software, IEEE, 2018, pp. 1–10.
LibreCat: https://research-explorer.ista.ac.at/record/5959
DOI: 10.1109/emsoft.2018.8537203
WoS: 000492828500005

Expectation optimization with probabilistic guarantees in POMDPs with discounted-sum objectives
K. Chatterjee, A. Elgyütt, P. Novotný, O. Rouillé, in:, IJCAI, 2018, pp. 4692–4699.
LibreCat: https://research-explorer.ista.ac.at/record/24
DOI: 10.24963/ijcai.2018/652
WoS: 000764175404117
arXiv: 1804.10601

An abstraction-refinement methodology for reasoning about network games
G. Avni, S. Guha, O. Kupferman, Games 9 (2018).
LibreCat: https://research-explorer.ista.ac.at/record/6006
DOI: 10.3390/g9030039

Contracts for system design
A. Benveniste, D. Nickovic, B. Caillaud, R. Passerone, J.B. Raclet, P. Reinkemeier, A. Sangiovanni-Vincentelli, W. Damm, T.A. Henzinger, K.G. Larsen, Foundations and Trends in Electronic Design Automation 12 (2018) 124–400.
LibreCat: https://research-explorer.ista.ac.at/record/5677
DOI: 10.1561/1000000053

A new proof rule for almost-sure termination
A. Mciver, C. Morgan, B.L. Kaminski, J.P. Katoen, Proceedings of the ACM on Programming Languages 2 (2017).
LibreCat: https://research-explorer.ista.ac.at/record/10418
DOI: 10.1145/3158121
arXiv: 1711.03588

Faster statistical model checking for unbounded temporal properties
P. Daca, T.A. Henzinger, J. Kretinsky, T. Petrov, ACM Transactions on Computational Logic (TOCL) 18 (2017).
LibreCat: https://research-explorer.ista.ac.at/record/471
DOI: 10.1145/3060139

Nested weighted automata
K. Chatterjee, T.A. Henzinger, J. Otop, ACM Transactions on Computational Logic (TOCL) 18 (2017).
LibreCat: https://research-explorer.ista.ac.at/record/467
DOI: 10.1145/3152769
arXiv: 1606.03598

Edit distance for pushdown automata
K. Chatterjee, T.A. Henzinger, R. Ibsen-Jensen, J. Otop, Logical Methods in Computer Science 13 (2017).
LibreCat: https://research-explorer.ista.ac.at/record/465
DOI: 10.23638/LMCS-13(3:23)2017

The cost of exactness in quantitative reachability
K. Chatterjee, L. Doyen, T.A. Henzinger, in:, L. Aceto, G. Bacci, A. Ingólfsdóttir, A. Legay, R. Mardare (Eds.), Models, Algorithms, Logics and Tools, Springer, 2017, pp. 367–381.
LibreCat: https://research-explorer.ista.ac.at/record/625
DOI: 10.1007/978-3-319-63121-9_18

Challenges and tool implementation of hybrid rapidly exploring random trees
S. Bak, S. Bogomolov, T.A. Henzinger, A. Kumar, in:, A. Abate, S. Bodo (Eds.), Springer, 2017, pp. 83–89.
LibreCat: https://research-explorer.ista.ac.at/record/633
DOI: 10.1007/978-3-319-63501-9_6

On the quantitative semantics of regular expressions over real-valued signals
A. Bakhirkin, T. Ferrere, O. Maler, D. Ulus, in:, A. Abate, G. Geeraerts (Eds.), Springer, 2017, pp. 189–206.
LibreCat: https://research-explorer.ista.ac.at/record/636
DOI: 10.1007/978-3-319-65765-3_11

Numerical Software Verification
S. Bogomolov, M. Martel, P. Prabhakar, eds., Numerical Software Verification, Springer, 2017.
LibreCat: https://research-explorer.ista.ac.at/record/638
DOI: 10.1007/978-3-319-54292-8

Synchronizing the asynchronous
T.A. Henzinger, B. Kragl, S. Qadeer, Synchronizing the Asynchronous, IST Austria, 2017.
LibreCat: https://research-explorer.ista.ac.at/record/6426
DOI: 10.15479/AT:IST-2018-853-v2-2

Safety verification of nonlinear hybrid systems based on invariant clusters
H. Kong, S. Bogomolov, C. Schilling, Y. Jiang, T.A. Henzinger, in:, Proceedings of the 20th International Conference on Hybrid Systems, ACM, 2017, pp. 163–172.
LibreCat: https://research-explorer.ista.ac.at/record/663
DOI: 10.1145/3049797.3049814

Bidirectional nested weighted automata
K. Chatterjee, T.A. Henzinger, J. Otop, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.
LibreCat: https://research-explorer.ista.ac.at/record/711
DOI: 10.4230/LIPIcs.CONCUR.2017.5

Timed network games with clocks
G. Avni, S. Guha, O. Kupferman, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.
LibreCat: https://research-explorer.ista.ac.at/record/963
DOI: 10.4230/LIPIcs.MFCS.2017.37

JFIX: Semantics-based repair of Java programs via symbolic  PathFinder
X. Le, D.H. Chu, D. Lo, C. Le Goues, W. Visser, in:, Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis, ACM, 2017, pp. 376–379.
LibreCat: https://research-explorer.ista.ac.at/record/941
DOI: 10.1145/3092703.3098225

Infinite-duration bidding games
G. Avni, T.A. Henzinger, V.K. Chonev, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.
LibreCat: https://research-explorer.ista.ac.at/record/950
DOI: 10.4230/LIPIcs.CONCUR.2017.21
arXiv: 1705.01433

Statistical and logical methods for property checking
P. Daca, Statistical and Logical Methods for Property Checking, Institute of Science and Technology Austria, 2017.
LibreCat: https://research-explorer.ista.ac.at/record/1155
DOI: 10.15479/AT:ISTA:TH_730

Conic abstractions for hybrid systems
S. Bogomolov, M. Giacobbe, T.A. Henzinger, H. Kong, in:, Springer, 2017, pp. 116–132.
LibreCat: https://research-explorer.ista.ac.at/record/647
DOI: 10.1007/978-3-319-65765-3_7

Counterexample guided refinement of template polyhedra
S. Bogomolov, G. Frehse, M. Giacobbe, T.A. Henzinger, in:, Springer, 2017, pp. 589–606.
LibreCat: https://research-explorer.ista.ac.at/record/631
DOI: 10.1007/978-3-662-54577-5_34

Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games
M. Svoreová, J. Kretinsky, M. Chmelik, K. Chatterjee, I. Cbrná, C. Belta, Nonlinear Analysis: Hybrid Systems 23 (2017) 230–253.
LibreCat: https://research-explorer.ista.ac.at/record/1407
DOI: 10.1016/j.nahs.2016.04.006
WoS: 000390637000014
arXiv: 1410.5387