Source: https://research-explorer.app.ist.ac.at/project/FD2A2D92-FDE9-11E8-8832-D63AE6697425
Timestamp: 2019-04-23 20:50:20+00:00

Document:
Over the past decades, the complexity and size as well as the ubiquity and criticality of computer systems have increased dramatically. They are now at a level where human engineers and programmers require assistance by computer-aided methods and tools that are based on a rigorous mathematical foundation. We have seen much recent progress in such techniques and tools: model checkers and static analyzers are now used routinely in the design of hardware and certain restricted kinds of software. Nevertheless, the exploding presence of concurrent computation - from multi-core processors to cloud computing - has rendered many established methods obsolete and is the single most important challenge facing systems engineering today. The traditional use of model checking and related techniques has been a posteriori, i.e., a program or model is analyzed after completion. This procedure is costly and decouples the quality assessment from the engineering process. It is the goal of our project to move beyond classical model checking and a posteriori verification. We use the term "Rigorous Systems Engineering" (RiSE) to describe an approach in which mathematical techniques such as model checking provide a solid foundation for the design process from day one. Within RiSE, we plan to focus on topics that are motivated by the new generation of highly concurrent and embedded systems: We will look at software transactions and data center programming to address multi-core and software-as-a-service issues; at virtualization and distributed message passing concepts to address real-time issues; and at the integration of model checking with complementary, execution based techniques, such as software testing, in order to build tools that can cope with large-scale software systems. The project has three main research thrusts: First, we will develop new language-based, architectural, and verification paradigms for highly concurrent and real-time software. Second, we will develop novel game-theoretic algorithms for analyzing and synthesizing individual system components within a larger context. Third, we will develop and improve decision procedures that lie at the very heart of every automatic method and tool for system design and analysis. RiSE consists of five internationally recognized researchers from the model checking community and four renowned researchers from the neighboring fields of software systems, distributed computing, and computational logic. This set-up will encourage the integration of different viewpoints and complementary approaches towards the common objective of RiSE.
K. Chatterjee, W. Dvorák, M. Henzinger, V. Loitzenbauer, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016.
K. Chatterjee, L. Doyen, in:, Schloss Dagstuhl- Leibniz-Zentrum fur Informatik, 2016.
K. Chatterjee, W. Dvoák, M. Henzinger, V. Loitzenbauer, in:, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, IEEE, 2016, pp. 197–206.
H. Kong, E. Bartocci, S. Bogomolov, R. Grosu, T.A. Henzinger, Y. Jiang, C. Schilling, in:, Springer, 2016, pp. 128–144.
G. Hofferek, A. Gupta, B. Könighofer, J. Jiang, R. Bloem, in:, 2013 Formal Methods in Computer-Aided Design, IEEE, 2013, pp. 77–84.
K. Chatterjee, M. Henzinger, V. Loitzenbauer, S. Oraee, V. Toman, in:, Springer, 2018, pp. 178–197.
U. Ahmed, K. Chatterjee, S. Gulwani, in:, AAAI Press, 2015, pp. 745–752.
V. Forejt, J. Krčál, J. Kretinsky, in:, Springer, 2015, pp. 162–177.
S. Bak, S. Bogomolov, T. Johnson, in:, Springer, 2015, pp. 128–133.
B. Kragl, S. Qadeer, in:, Springer, 2018, pp. 79–102.
M. Giacobbe, C.C. Guet, A. Gupta, T.A. Henzinger, T. Paixao, T. Petrov, 9035 (2015) 469–483.
R. Blanc, A. Gupta, L. Kovács, B. Kragl, 8312 (2013) 173–181.
Y. Godhal, K. Chatterjee, T.A. Henzinger, International Journal on Software Tools for Technology Transfer 15 (2013) 585–601.
T.A. Henzinger, in:, Conference Proceedings MODELS 2012, Springer, 2012, pp. 1–2.
P. Cerny, S. Gopi, T.A. Henzinger, A. Radhakrishna, N. Totla, in:, Proceedings of the Tenth ACM International Conference on Embedded Software, ACM, 2012, pp. 53–62.
K. Chatterjee, V. Prabhu, in:, Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control, Springer, 2013, pp. 273–282.
T. Brázdil, K. Chatterjee, J. Kretinsky, V. Toman, in:, Springer, 2018, pp. 385–407.
K. Chatterjee, L. Doyen, Theoretical Computer Science 458 (2012) 49–60.
K. Chatterjee, Information and Computation 211 (2012) 29–48.
K. Chatterjee, V. Prabhu, in:, Springer, 2011, pp. 221–230.
K. Chatterjee, R. Majumdar, in:, U. Fahrenberg, S. Tripakis (Eds.), Springer, 2011, pp. 145–159.
K. Chatterjee, Z. Komárková, J. Kretinsky, (2015) 244–256.
K. Chatterjee, M. Henzinger, in:, Proceedings of the Annual ACM-SIAM Symposium on Discrete Algorithms, SIAM, 2012, pp. 1386–1399.
K. Chatterjee, A.K. Goharshady, A. Pourdamghani, in:, IEEE International Conference on Blockchain and Cryptocurrency, IEEE, n.d.
G. Avni, S. Guha, O. Kupferman, Games 9 (2018).
G. Avni, O. Kupferman, Theoretical Computer Science 712 (2018) 50–72.
D. Zufferey, Analysis of Dynamic Message Passing Programs, IST Austria, 2013.
P. Daca, T.A. Henzinger, J. Kretinsky, T. Petrov, in:, Springer, 2016, pp. 112–129.
K. Chatterjee, M. Chmelik, P. Daca, Formal Methods in System Design 47 (2015) 230–264.
K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, P. Goyal, ACM SIGPLAN Notices 50 (2015) 97–109.
C. Dragoi, T.A. Henzinger, H. Veith, J. Widder, D. Zufferey, in:, Springer, 2014, pp. 161–181.
C. Hilbe, L. Schmid, J. Tkadlec, K. Chatterjee, M. Nowak, PNAS 115 (2018) 12241–12246.
K. Chatterjee, R. Ibsen-Jensen, A. Pavlogiannis, in:, Springer, 2015, pp. 140–157.
L. D’Antoni, R. Samanta, R. Singh, in:, Springer, 2016, pp. 383–401.
K. Hansen, R. Ibsen-Jensen, M. Koucký, in:, Springer, 2016, pp. 64–76.
C. Dragoi, T.A. Henzinger, D. Zufferey, in:, ACM, 2016, pp. 400–415.
T. Ferrere, in:, Springer, 2018, pp. 147–164.
A. Pavlogiannis, K. Chatterjee, B. Adlam, M. Nowak, Scientific Reports 5 (2015).
S. Bogomolov, C. Schilling, E. Bartocci, G. Batt, H. Kong, R. Grosu, in:, Springer, 2015, pp. 19–35.
Y. Velner, K. Chatterjee, L. Doyen, T.A. Henzinger, A. Rabinovich, J. Raskin, Information and Computation 241 (2015) 177–196.
T. Priklopil, K. Chatterjee, Games 6 (2015) 413–437.
C. Schilling, S. Bogomolov, T.A. Henzinger, A. Podelski, J. Ruess, Biosystems 149 (2016) 15–25.
A. Bakhirkin, T. Ferrere, O. Maler, in:, Association for Computing Machinery, Inc, 2018, pp. 177–186.
R. Bloem, K. Chatterjee, S. Jacobs, R. Könighofer, in:, Springer, 2015, pp. 517–532.
K. Chatterjee, D. Zufferey, M. Nowak, Journal of Theoretical Biology 301 (2012) 161–173.
K. Chatterjee, W. Dvorák, M. Henzinger, V. Loitzenbauer, in:, ACM, 2018, pp. 2341–2356.
A. Gupta, C. Popeea, A. Rybalchenko, in:, H. Yang (Ed.), Springer, 2011, pp. 188–203.
K. Chatterjee, V. Raman, in:, Springer, 2012, pp. 152–168.
T. Brázdil, V. Brožek, K. Chatterjee, V. Forejt, A. Kučera, in:, IEEE, 2011.
U. Boker, T.A. Henzinger, in:, Springer, 2011, pp. 82–96.
K. Chatterjee, L. Doyen, in:, IEEE, 2016, pp. 247–256.
K. Chatterjee, S. Chaubal, P. Kamath, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012, pp. 167–182.
K. Chatterjee, Y. Velner, in:, Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science, IEEE, 2012.
U. Boker, K. Chatterjee, T.A. Henzinger, O. Kupferman, Temporal Specifications with Accumulative Values, IST Austria, 2011.
K. Chatterjee, H. Fu, P. Novotný, R. Hasheminezhad, ACM Transactions on Programming Languages and Systems 40 (2018).
M. Christakis, M. Heizmann, M.N. Mansur, C. Schilling, V. Wüstholz, in:, T. Vojnar, L. Zhang (Eds.), 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems , Springer, 2019.
K. Chatterjee, R. Ibsen-Jensen, A.K. Goharshady, A. Pavlogiannis, ACM Transactions on Programming Languages and Systems 40 (2018).
K. Chatterjee, T.A. Henzinger, J. Otop, in:, M. Lohstroh, P. Derler, M. Sirjani (Eds.), Principles of Modeling, Springer, 2018, pp. 143–161.
K. Chatterjee, A. Pavlogiannis, A. Kößler, U. Schmid, Real-Time Systems 54 (2018) 166–207.
S. Bogomolov, M. Forets, G. Frehse, K. Potomkin, C. Schilling, in:, N. Ozay, P. Prabhakar (Eds.), Proceedings of the 22nd International Conference on Hybrid Systems: Computation and Control, ACM, New York, NY, USA, n.d., p. 7.
K. Chatterjee, A. Elgyütt, P. Novotny, O. Rouillé, in:, IJCAI, 2018, pp. 4692–4699.
P. Daca, Statistical and Logical Methods for Property Checking, IST Austria, 2017.
B. Zagorsky, J. Reiter, K. Chatterjee, M. Nowak, PLoS One 8 (2013).
A. Fellner, Experimental Part of CAV 2015 Publication: Counterexample Explanation by Learning Small Strategies in Markov Decision Processes, IST Austria, 2015.
K. Chatterjee, R. Ibsen-Jensen, J. Tkadlec, in:, AAAI Press, 2016, pp. 172–179.
K. Chatterjee, P. Novotny, D. Zikelic, in:, ACM, 2017, pp. 145–160.
D. Beyer, T.A. Henzinger, M. Keremoglu, P. Wendler, in:, Proceedings of the ACM SIGSOFT 20th International Symposium on the Foundations of Software Engineering, ACM, 2012.
V.K. Chonev, J. Ouaknine, J. Worrell, in:, LICS ’16, IEEE, 2016, pp. 515–524.
G. Frehse, M. Giacobbe, T.A. Henzinger, in:, Springer, 2018, pp. 468–486.
T. Brázdil, K. Chatterjee, M. Chmelik, A. Gupta, P. Novotny, in:, Proceedings of the 15th International Conference on Autonomous Agents and Multiagent Systems, ACM, 2016, pp. 1465–1466.
B. Kragl, S. Qadeer, T.A. Henzinger, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018.
G. Avni, T.A. Henzinger, O. Kupferman, in:, Springer, 2016, pp. 153–166.
C. Hilbe, Š. Šimsa, K. Chatterjee, M. Nowak, Nature 559 (2018) 246–249.
T. Babiak, F. Blahoudek, A. Duret Lutz, J. Klein, J. Kretinsky, D. Mueller, D. Parker, J. Strejček, in:, Springer, 2015, pp. 479–486.
L. Nguyen, C. Schilling, S. Bogomolov, T. Johnson, 9333 (2015) 281–286.
S. Bogomolov, D. Magazzeni, S. Minopoli, M. Wehrle, in:, AAAI Press, 2015, pp. 42–46.
K. Chatterjee, V. Prabhu, IEEE Transactions on Automatic Control 60 (2015) 2291–2306.
E. Bartocci, T. Ferrere, N. Manjunath, D. Nickovic, in:, Association for Computing Machinery, Inc, 2018, pp. 197–206.
N. Beneš, J. Kretinsky, K. Larsen, M. Möller, S. Sickert, J. Srba, Acta Informatica 52 (2015) 269–297.
T. Brázdil, K. Chatterjee, V. Forejt, A. Kučera, 9035 (2015) 181–187.
C. Dragoi, C. Enea, M. Sighireanu, in:, Springer, 2013, pp. 150–171.
A. Desai, V. Gupta, E. Jackson, S. Qadeer, S. Rajamani, D. Zufferey, in:, Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation, ACM, 2013, pp. 321–331.
K. Chatterjee, A. Goharshady, Y. Velner, in:, Springer, 2018, pp. 739–767.
K. Chatterjee, N. Fijalkow, in:, A.-H. Dediu, S. Inenaga, C. Martín-Vide (Eds.), Springer, 2011, pp. 216–226.
P. Cerny, K. Chatterjee, T.A. Henzinger, in:, IEEE, 2011, pp. 205–217.
K. Chatterjee, M. Henzinger, M. Joglekar, S. Nisarg, in:, G. Gopalakrishnan, S. Qadeer (Eds.), Springer, 2011, pp. 260–276.
K. Chatterjee, L. De Alfaro, T.A. Henzinger, ACM Transactions on Computational Logic (TOCL) 12 (2011).
P. Cerny, K. Chatterjee, T.A. Henzinger, A. Radhakrishna, R. Singh, in:, G. Gopalakrishnan, S. Qadeer (Eds.), Springer, 2011, pp. 243–259.
K. Chatterjee, M. Tracol, in:, Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science, IEEE, 2012.
C. Dragoi, A. Gupta, T.A. Henzinger, in:, Computer Aided Verification, Springer Berlin Heidelberg, Berlin, Heidelberg, 2013, pp. 174–190.
K. Chatterjee, A. Kößler, U. Schmid, in:, Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control, ACM, 2013, pp. 163–172.
G. Avni, T.A. Henzinger, V.K. Chonev, in:, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.
K. Horák, B. Bošanský, K. Chatterjee, in:, Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI, 2018, pp. 4764–4770.

References: V. 
 V. 
 V. 
 V. 

V. 
 V. 
 V. 
 V. 
 V. 
 V. 
 V. 
 V. 
 V. 
 V. 
 V. 
 V.