Automated verification: graphs, logic, and automata
作者： Moshe Y. Vardi
DOI:
关键词:
摘要: Automated verification is one of the most successful applications automated reasoning in computer science. In uses algorithmic techniques to establish correctness design with respect a given property. based on small number key ideas, tying together graph theory, automata and logic. this self-contained talk I will describe how "holy trinity" gave rise automated-verification tools, mention some planning.
ijcai.org参考文章(26)
Moshe Y. Vardi, Diego Calvanese, Giuseppe De Giacomo, Reasoning about actions and planning in LTL action theories principles of knowledge representation and reasoning. pp. 593- 602 ,(2002)
Moshe Y. Vardi, Branching vs. Linear Time: Final Showdown tools and algorithms for construction and analysis of systems. pp. 1- 22 ,(2001) , 10.1007/3-540-45319-9_1
Fady Copty, Limor Fix, Ranan Fraer, Enrico Giunchiglia, Gila Kamhi, Armando Tacchella, Moshe Y. Vardi, Benefits of Bounded Model Checking at an Industrial Setting computer aided verification. pp. 436- 453 ,(2001) , 10.1007/3-540-44585-4_43
Moshe Y. Vardi, An automata-theoretic approach to linear temporal logic Proceedings of the VIII Banff Higher order workshop conference on Logics for concurrency : structure versus automata: structure versus automata. pp. 238- 266 ,(1996) , 10.1007/3-540-60915-6_6
Giuseppe De Giacomo, Moshe Y. Vardi, Automata-Theoretic Approach to Planning for Temporally Extended Goals Lecture Notes in Computer Science. pp. 226- 238 ,(1999) , 10.1007/10720246_18
Fahiem Bacchus, Froduald Kabanza, Planning for temporally extended goals Annals of Mathematics and Artificial Intelligence. ,vol. 22, pp. 5- 27 ,(1998) , 10.1023/A:1018985923441
J. P. Queille, J. Sifakis, Specification and verification of concurrent systems in CESAR Proceedings of the 5th Colloquium on International Symposium on Programming. pp. 337- 351 ,(1982) , 10.1007/3-540-11494-7_22
Robert P. Kurshan, Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach ,(1995)
Bart Selman, Henry Kautz, Planning as satisfiability european conference on artificial intelligence. pp. 359- 363 ,(1992)
A. Cimatti, M. Roveri, Conformant planning via symbolic model checking Journal of Artificial Intelligence Research. ,vol. 13, pp. 305- 338 ,(2000) , 10.1613/JAIR.774