Bogomolov S, Martel M, Prabhakar P, eds. Numerical Software Verification. Vol 10152. Springer; 2017. doi:10.1007/978-3-319-54292-8

Henzinger TA, Kragl B, Qadeer S. Synchronizing the Asynchronous. IST Austria; 2017. doi:10.15479/AT:IST-2018-853-v2-2

Kong H, Bogomolov S, Schilling C, Jiang Y, Henzinger TA. Safety verification of nonlinear hybrid systems based on invariant clusters. In: Proceedings of the 20th International Conference on Hybrid Systems. ACM; 2017:163-172. doi:10.1145/3049797.3049814

Chatterjee K, Henzinger TA, Otop J. Bidirectional nested weighted automata. In: Vol 85. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2017. doi:10.4230/LIPIcs.CONCUR.2017.5

Avni G, Guha S, Kupferman O. Timed network games with clocks. In: Vol 83. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2017. doi:10.4230/LIPIcs.MFCS.2017.37

Le X, Chu DH, Lo D, Le Goues C, Visser W. JFIX: Semantics-based repair of Java programs via symbolic  PathFinder. In: Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis. ACM; 2017:376-379. doi:10.1145/3092703.3098225

Avni G, Henzinger TA, Chonev VK. Infinite-duration bidding games. In: Vol 85. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2017. doi:10.4230/LIPIcs.CONCUR.2017.21

Daca P. Statistical and logical methods for property checking. 2017. doi:10.15479/AT:ISTA:TH_730

Bogomolov S, Giacobbe M, Henzinger TA, Kong H. Conic abstractions for hybrid systems. In: Vol 10419. Springer; 2017:116-132. doi:10.1007/978-3-319-65765-3_7

Bogomolov S, Frehse G, Giacobbe M, Henzinger TA. Counterexample guided refinement of template polyhedra. In: Vol 10205. Springer; 2017:589-606. doi:10.1007/978-3-662-54577-5_34

Svoreová M, Kretinsky J, Chmelik M, Chatterjee K, Cbrná I, Belta C. Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. Nonlinear Analysis: Hybrid Systems. 2017;23(2):230-253. doi:10.1016/j.nahs.2016.04.006

Cerny P, Clarke E, Henzinger TA, et al. From non-preemptive to preemptive scheduling using synchronization synthesis. Formal Methods in System Design. 2017;50(2-3):97-139. doi:10.1007/s10703-016-0256-5

Giacobbe M, Guet CC, Gupta A, Henzinger TA, Paixao T, Petrov T. Model checking the evolution of gene regulatory networks. Acta Informatica. 2017;54(8):765-787. doi:10.1007/s00236-016-0278-x

Henzinger TA, Otop J. Model measuring for discrete and hybrid systems. Nonlinear Analysis: Hybrid Systems. 2017;23:166-190. doi:10.1016/j.nahs.2016.09.001

Avni G, Goel S, Henzinger TA, Rodríguez Navas G. Computing scores of forwarding schemes in switched networks with probabilistic faults. In: Vol 10206. Springer; 2017:169-187. doi:10.1007/978-3-662-54580-5_10

Chatterjee K, Henzinger TA, Otop J, Velner Y. Quantitative fair simulation games. Information and Computation. 2017;254(2):143-166. doi:10.1016/j.ic.2016.10.006

Chatterjee K, Kragl B, Mishra S, Pavlogiannis A. Faster algorithms for weighted recursive state machines. In: Yang H, ed. Vol 10201. Springer; 2017:287-313. doi:10.1007/978-3-662-54434-1_11

Avni G, Guha S, Kupferman O. An abstraction-refinement methodology for reasoning about network games. In: AAAI Press; 2017:70-76. doi:10.24963/ijcai.2017/11

Trinh M, Chu DH, Jaffar J. Model counting for recursively-defined strings. In: Majumdar R, Kundak V, eds. Vol 10427. Springer; 2017:399-418. doi:10.1007/978-3-319-63390-9_21

Le X, Chu DH, Lo D, Le Goues C, Visser W. : Syntax- and semantic-guided repair synthesis via programming by examples. In: Vol 0154. ACM; 2017:593-604. doi:10.1145/3106237.3106309

Gottlob G, Henzinger TA, Weißenbacher G. Preface of the special issue in memoriam Helmut Veith. Formal Methods in System Design. 2017;51(2):267-269. doi:10.1007/s10703-017-0307-6

Finkbeiner B, Kupriyanov A. Causality-based model checking. In: Electronic Proceedings in Theoretical Computer Science. Vol 259. Open Publishing Association; 2017:31-38. doi:10.4204/EPTCS.259.3

Chatterjee K, Henzinger TA, Otop J. Nested weighted limit-average automata of bounded width. In: Vol 58. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2016. doi:10.4230/LIPIcs.MFCS.2016.24

Haas A, Henzinger TA, Holzer A, et al. Local linearizability for concurrent container-type data structures. In: Leibniz International Proceedings in Informatics. Vol 59. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2016. doi:10.4230/LIPIcs.CONCUR.2016.6

Gurung A, Deka A, Bartocci E, Bogomolov S, Grosu R, Ray R. Parallel reachability analysis for hybrid systems. In: IEEE; 2016. doi:10.1109/MEMCOD.2016.7797741

Avni G, Guha S, Rodríguez Navas G. Synthesizing time triggered schedules for switched networks with faulty links. In: Proceedings of the 13th International Conference on Embedded Software . ACM; 2016. doi:10.1145/2968478.2968499

Duggirala P, Fan C, Potok M, et al. Tutorial: Software tools for hybrid systems verification transformation and synthesis10.1109/CCA.2016.7587948__HyST and TuLiP. In: 2016 IEEE Conference on Control Applications. IEEE; 2016. doi:10.1109/CCA.2016.7587948

Chatterjee K, Henzinger TA, Otop J. Quantitative automata under probabilistic semantics. In: Proceedings of the 31st Annual ACM/IEEE Symposium. IEEE; 2016:76-85. doi:10.1145/2933575.2933588

Kong H, Bartocci E, Bogomolov S, et al. Discrete abstraction of multiaffine systems. In: Vol 9957. Springer; 2016:128-144. doi:10.1007/978-3-319-47151-8_9

Jiang Y, Yang Y, Liu H, et al. From stateflow simulation to verified implementation: A verification approach and a real-time train controller design. In: IEEE; 2016. doi:10.1109/RTAS.2016.7461337

Chatterjee K, Henzinger TA, Otop J. Quantitative monitor automata. In: Vol 9837. Springer; 2016:23-38. doi:10.1007/978-3-662-53413-7_2

D’Antoni L, Samanta R, Singh R. QLOSE: Program repair with quantitative objectives. In: Vol 9780. Springer; 2016:383-401. doi:10.1007/978-3-319-41540-6_21

Bak S, Bogomolov S, Henzinger TA, Johnson T, Prakash P. Scalable static hybridization methods for analysis of nonlinear systems. In: Springer; 2016:155-164. doi:10.1145/2883817.2883837

Dragoi C, Henzinger TA, Zufferey D. PSYNC: A partially synchronous language for fault-tolerant distributed algorithms. In: Vol 20-22. ACM; 2016:400-415. doi:10.1145/2837614.2837650

Beica A, Guet CC, Petrov T. Efficient reduction of kappa models by static inspection of the rule-set. In: Vol 9271. Springer; 2016:173-191. doi:10.1007/978-3-319-26916-0_10

Henzinger TA, Otop J, Samanta R. Lipschitz robustness of timed I/O systems. In: Vol 9583. Springer; 2016:250-267. doi:10.1007/978-3-662-49122-5_12

Schilling C, Bogomolov S, Henzinger TA, Podelski A, Ruess J. Adaptive moment closure for parameter inference of biochemical reaction networks. Biosystems. 2016;149:15-25. doi:10.1016/j.biosystems.2016.07.005

Bogomolov S, Donzé A, Frehse G, et al. Guided search for hybrid systems based on coarse-grained space abstractions. International Journal on Software Tools for Technology Transfer. 2016;18(4):449-467. doi:10.1007/s10009-015-0393-y

Jiang Y, Liu H, Kong H, et al. Use runtime verification to improve the quality of medical care practice. In: Proceedings of the 38th International Conference on Software Engineering Companion . IEEE; 2016:112-121. doi:10.1145/2889160.2889233

Chatterjee K, Chmelik M, Davies J. A symbolic SAT based algorithm for almost sure reachability with small strategies in pomdps. In: Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence. Vol 2016. AAAI Press; 2016:3225-3232.

Avni G, Henzinger TA, Kupferman O. Dynamic resource allocation games. In: Vol 9928. Springer; 2016:153-166. doi:10.1007/978-3-662-53354-3_13

Tarrach T. Automatic synthesis of synchronisation primitives for concurrent programs. 2016. doi:10.15479/at:ista:1130

Daca P, Henzinger TA, Kretinsky J, Petrov T. Linear distances between Markov chains. In: Vol 59. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2016. doi:10.4230/LIPIcs.CONCUR.2016.20

Daca P, Henzinger TA, Kretinsky J, Petrov T. Faster statistical model checking for unbounded temporal properties. In: Vol 9636. Springer; 2016:112-129. doi:10.1007/978-3-662-49674-9_7

Daca P, Gupta A, Henzinger TA. Abstraction-driven concolic testing. In: Vol 9583. Springer; 2016:328-347. doi:10.1007/978-3-662-49122-5_16

Daca P, Henzinger TA, Kupriyanov A. Array folds logic. In: Vol 9780. Springer; 2016:230-248. doi:10.1007/978-3-319-41540-6_13

Jiang Y, Liu H, Song H, et al. Safety assured formal model driven design of the multifunction vehicle bus controller. In: Vol 9995. Springer; 2016:757-763. doi:10.1007/978-3-319-48989-6_47

Parise F, Lygeros J, Ruess J. Bayesian inference for stochastic individual-based models of ecological systems: a pest control simulation study. Frontiers in Environmental Science. 2015;3. doi:10.3389/fenvs.2015.00042

Dragoi C, Henzinger TA, Zufferey D. The need for language support for fault-tolerant distributed systems. 2015;32:90-102. doi:10.4230/LIPIcs.SNAPL.2015.90

Kretinsky J, Larsen K, Laursen S, Srba J. Polynomial time decidability of weighted synchronization under partial observability. In: Vol 42. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2015:142-154. doi:10.4230/LIPIcs.CONCUR.2015.142

Ruess J. Minimal moment equations for stochastic models of biochemical reaction networks with partially finite state space. Journal of Chemical Physics. 2015;143(24). doi:10.1063/1.4937937

Ruess J, Parise F, Milias Argeitis A, Khammash M, Lygeros J. Iterative experiment design guides the characterization of a light-inducible gene expression circuit. PNAS. 2015;112(26):8148-8153. doi:10.1073/pnas.1423947112

Ray R, Gurung A, Das B, Bartocci E, Bogomolov S, Grosu R. XSpeed: Accelerating reachability analysis on multi-core processors. 2015;9434:3-18. doi:10.1007/978-3-319-26287-1_1

Forejt V, Krdál J, Kretinsky J. Controller synthesis for MDPs and frequency LTL\'47U. In: Vol 9450. Springer; 2015:162-177. doi:10.1007/978-3-662-48899-7_12

Babiak T, Blahoudek F, Duret Lutz A, et al. The Hanoi omega-automata format. In: Vol 9206. Springer; 2015:479-486. doi:10.1007/978-3-319-21690-4_31

Bogomolov S, Schilling C, Bartocci E, Batt G, Kong H, Grosu R. Abstraction-based parameter synthesis for multiaffine systems. In: Vol 9434. Springer; 2015:19-35. doi:10.1007/978-3-319-26287-1_2

Nguyen L, Schilling C, Bogomolov S, Johnson T. Runtime verification for hybrid analysis tools. In: 6th International Conference. Vol 9333. Springer Nature; 2015:281-286. doi:10.1007/978-3-319-23820-3_19

Bogomolov S, Henzinger TA, Podelski A, Ruess J, Schilling C. Adaptive moment closure for parameter inference of biochemical reaction networks. 2015;9308:77-89. doi:10.1007/978-3-319-23401-4_8

Bogomolov S, Magazzeni D, Minopoli S, Wehrle M. PDDL+ planning with hybrid automata: Foundations of translating must behavior. In: AAAI Press; 2015:42-46.

Michaliszyn J, Otop J, Kieroski E. On the decidability of elementary modal logics. ACM Transactions on Computational Logic. 2015;17(1). doi:10.1145/2817825

Frehse G, Bogomolov S, Greitschus M, Strump T, Podelski A. Eliminating spurious transitions in reachability with support functions. In: Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control. ACM; 2015:149-158. doi:10.1145/2728606.2728622

Bak S, Bogomolov S, Johnson T. HYST: A source transformation and translation tool for hybrid automaton models. In: Springer; 2015:128-133. doi:10.1145/2728606.2728630

Velner Y, Chatterjee K, Doyen L, Henzinger TA, Rabinovich A, Raskin J. The complexity of multi-mean-payoff and multi-energy games. Information and Computation. 2015;241(4):177-196. doi:10.1016/j.ic.2015.03.001

Gupta A, Henzinger TA. Guest editors’ introduction to special issue on computational methods in systems biology. ACM Transactions on Modeling and Computer Simulation. 2015;25(2). doi:10.1145/2745799

Cerny P, Henzinger TA, Kovács L, Radhakrishna A, Zwirchmayr J. Segment abstraction for worst-case execution time analysis. 2015;9032:105-131. doi:10.1007/978-3-662-46669-8_5

Benes N, Kretinsky J, Larsen K, Möller M, Sickert S, Srba J. Refinement checking on parametric modal transition systems. Acta Informatica. 2015;52(2-3):269-297. doi:10.1007/s00236-015-0215-4

Geiger B, Petrov T, Kubin G, Koeppl H. Optimal Kullback-Leibler aggregation via information bottleneck. IEEE Transactions on Automatic Control. 2015;60(4):1010-1022. doi:10.1109/TAC.2014.2364971

Ruess J, Lygeros J. Moment-based methods for parameter inference and experiment design for stochastic biochemical reaction networks. ACM Transactions on Modeling and Computer Simulation. 2015;25(2). doi:10.1145/2688906

Henzinger TA, Raskin J. The equivalence problem for finite automata: Technical perspective. Communications of the ACM. 2015;58(2):86-86. doi:10.1145/2701001

Fahrenberg U, Kretinsky J, Legay A, Traonouez L. Compositionality for quantitative specifications. In: Vol 8997. Springer; 2015:306-324. doi:10.1007/978-3-319-15317-9_19

Gupta A, Henzinger TA, Radhakrishna A, Samanta R, Tarrach T. Succinct representation of concurrent trace sets. In: ACM; 2015:433-444. doi:10.1145/2676726.2677008

Chakraborty S, Henzinger TA, Sezgin A, Vafeiadis V. Aspect-oriented linearizability proofs. Logical Methods in Computer Science. 2015;11(1). doi:10.2168/LMCS-11(1:20)2015

Chatterjee K, Doyen L, Gimbert H, Henzinger TA. Randomness for free. Information and Computation. 2015;245(12):3-16. doi:10.1016/j.ic.2015.06.003

Chatterjee K, Henzinger TA, Jobstmann B, Singh R. Measuring and synthesizing systems in probabilistic environments. Journal of the ACM. 2015;62(1). doi:10.1145/2699430

Chatterjee K, Komárková Z, Kretinsky J. Unifying two views on multiple mean-payoff objectives in Markov decision processes. 2015:244-256. doi:10.1109/LICS.2015.32

Chatterjee K, Henzinger TA, Otop J. Nested weighted automata. In: Proceedings - Symposium on Logic in Computer Science. Vol 2015-July. IEEE; 2015. doi:10.1109/LICS.2015.72

Chatterjee K, Henzinger TA, Otop J. Nested Weighted Automata. IST Austria; 2015. doi:10.15479/AT:IST-2015-170-v2-2

Boker U, Henzinger TA, Otop J. The target discounted-sum problem. In: LICS. Logic in Computer Science. IEEE; 2015:750-761. doi:10.1109/LICS.2015.74

Chatterjee K, Henzinger TA, Ibsen-Jensen R, Otop J. Edit distance for pushdown automata. In: 42nd International Colloquium. Vol 9135. Springer Nature; 2015:121-133. doi:10.1007/978-3-662-47666-6_10

Boker U, Henzinger TA, Otop J. The Target Discounted-Sum Problem. IST Austria; 2015. doi:10.15479/AT:IST-2015-335-v1-1

Benes N, Daca P, Henzinger TA, Kretinsky J, Nickovic D. Complete composition operators for IOCO-testing theory. In: ACM; 2015:101-110. doi:10.1145/2737166.2737175

Chatterjee K, Chmelik M, Daca P. CEGAR for compositional analysis of qualitative properties in Markov decision processes. Formal Methods in System Design. 2015;47(2):230-264. doi:10.1007/s10703-015-0235-2

Svoreová M, Kretinsky J, Chmelik M, Chatterjee K, Cbrná I, Belta C. Temporal logic control for stochastic linear systems using abstraction refinement of probabilistic games. In: Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control. ACM; 2015:259-268. doi:10.1145/2728606.2728608

Cerny P, Clarke E, Henzinger TA, et al. From non-preemptive to preemptive scheduling using synchronization synthesis. 2015;9207:180-197. doi:10.1007/978-3-319-21668-3_11

Giacobbe M, Guet CC, Gupta A, Henzinger TA, Paixao T, Petrov T. Model checking gene regulatory networks. 2015;9035:469-483. doi:10.1007/978-3-662-46681-0_47

Brázdil T, Chatterjee K, Chmelik M, Fellner A, Kretinsky J. Counterexample explanation by learning small strategies in Markov decision processes. In: Vol 9206. Springer; 2015:158-177. doi:10.1007/978-3-319-21690-4_10

Dragoi C, Henzinger TA, Veith H, Widder J, Zufferey D. A logic-based framework for verifying consensus algorithms. In: Vol 8318. Springer; 2014:161-181. doi:10.1007/978-3-642-54013-4_10

Gordon A, Henzinger TA, Nori A, Rajamani S. Probabilistic programming. In: Proceedings of the on Future of Software Engineering. ACM; 2014:167-181. doi:10.1145/2593882.2593900

Gupta A, Popeea C, Rybalchenko A. Generalised interpolation by solving recursion free-horn clauses. In: Electronic Proceedings in Theoretical Computer Science, EPTCS. Vol 169. Open Publishing; 2014:31-38. doi:10.4204/EPTCS.169.5

Hofferek G, Gupta A. Suraq - a controller synthesis tool using uninterpreted functions. In: Yahav E, ed. HVC 2014. Vol 8855. Springer; 2014:68-74. doi:10.1007/978-3-319-13338-6_6

Gupta A, Kovács L, Kragl B, Voronkov A. Extensional crisis and proving identity. In: Cassez F, Raskin J-F, eds. ATVA 2014. Vol 8837. Springer; 2014:185-200. doi:10.1007/978-3-319-11936-6_14

Henzinger TA, Otop J, Samanta R. Lipschitz robustness of finite-state transducers. In: Leibniz International Proceedings in Informatics, LIPIcs. Vol 29. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2014:431-443. doi:10.4230/LIPIcs.FSTTCS.2014.431

Samanta R, Olivo O, Allen E. Cost-aware automatic program repair. In: Müller-Olm M, Seidl H, eds. Vol 8723. Springer; 2014:268-284. doi:10.1007/978-3-319-10936-7_17

Brázdil T, Chatterjee K, Chmelik M, et al. Verification of markov decision processes using learning algorithms. In: Cassez F, Raskin J-F, eds. 10.1007/978-3-319-11936-6_8__Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol 8837. Society of Industrial and Applied Mathematics; 2014:98-114. doi:10.1007/978-3-319-11936-6_8

Komárková Z, Kretinsky J. Rabinizer 3: Safraless translation of ltl to small deterministic automata. In: Cassez F, Raskin J-F, eds. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol 8837. Springer; 2014:235-241. doi:10.1007/978-3-319-11936-6_17

Hermanns H, Krdál J, Kretinsky J. Probabilistic bisimulation: Naturally on distributions. In: Baldan P, Gorla D, eds. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol 8704. Schloss Dagstuhl - Leibniz-Zentrum für Informatik; 2014:249-265. doi:10.1007/978-3-662-44584-6_18

Ganguly A, Petrov T, Koeppl H. Markov chain aggregation and its applications to combinatorial reaction networks. Journal of Mathematical Biology. 2014;69(3):767-797. doi:10.1007/s00285-013-0738-7

Bloem R, Chatterjee K, Greimel K, et al. Synthesizing robust systems. Acta Informatica. 2014;51(3-4):193-220. doi:10.1007/s00236-013-0191-5

Esparza J, Kretinsky J. From LTL to deterministic automata: A safraless compositional approach. In: Vol 8559. Springer; 2014:192-208. doi:10.1007/978-3-319-08867-9_13

Boker U, Henzinger TA. Exact and approximate determinization of discounted-sum automata. Logical Methods in Computer Science. 2014;10(1). doi:10.2168/LMCS-10(1:10)2014