Learning to verify branching time properties
Tóm tắt
Từ khóa
Tài liệu tham khảo
1. Abdulla PA, Jonsson B, Nilsson M, d'Orso J (2003) Algorithmic improvements in regular model checking. In: Computer-Aided verification (CAV′03), LNCS, vol 2725, Springer, pp 236–248
2. Alur R, Cerny P, Madhusudan P, Nam W (2005) Synthesis of interface specifications for Java classes. In: 2nd ACM SIGPLAN-SIGACT symposium on principles of program languages
3. Alur R, Madhusudan P, Nam W (2005) Symbolic compositional verification by learning assumptions. In: Proceedings of the 17th international conference on computer aided verification
4. ALV (2004) Action language verifier. http://www.cs.ucsb.edu/~bultan/composite/
6. Angluin D (1987) Learning regular sets from queries and counterexamples. Inform Comput 75(2):87–106
7. Annichini A, Bouajjani A, Sighireanu M (2001) TReX: a tool for reachability analysis of complex systems. In: Berry G, Comon H, Finkel A (eds) Proceedings of the international conference on computer aided verification (CAV′01), lecture notes in computer science, vol 1855, Springer, Paris, France
8. Bardin S, Finkel A, Leroux J (2004) FASTer acceleration of counter automata in practice. In: Jensen K, Podelski A (eds) Proceedings of the 10th international conference on tools and algorithms for construction and analysis of systems (TACAS′04), lecture notes in computer science, vol 2988. Springer, Barcelona, Spain, pp 576–590
11. Boigelot B (1999) Symbolic methods for exploring infinite state spaces. PhD thesis, Collection des Publications de la Faculté des Sciences Appliquées de l'Université de Liége
12. Boigelot B, Legay A, Wolper P (2003) Iterating transducers in the large (extended abstract). In: CAV: International conference on computer aided verification
13. Bouajjani A, Jonsson B, Nilsson M, Touili T (2000) Regular model checking. In: Emerson EA, Sistla AP (eds) Proceedings of the 12th International Conference on Computer-Aided Verification (CAV′00), LNCS, vol 1855, Springer, pp 403–418
14. Bultan T (1998) Automated symbolic analysis of reactive systems. PhD thesis, Department of Computer Science, University of Maryland, College Park, MD
15. Bultan T, Gerber R, Pugh W (1997) Symbolic model checking of infinite state programs using presburger arithmetic. In: Proceedings of the 9th international conference on computer aided verification (CAV 1997). pp 400–411
16. Bultan T, Yavuz-Kahveci T (2001) Action language verifier. In: Proceedings of the 16th IEEE International Conference on Automated Software Engineering, pp 382–386
17. Clarke E, Chaki S, Sinha N, Thati P (2005) Automated assume-guarantee reasoning for simulation conformance. In: Proceedings of the 17th International Conference on Computer Aided Verification
18. Clarke EM, Grumberg O, Peled DA (2000) Model checking. Number ISBN:0262032708. The MIT Press
19. Cobleigh JM, Giannakopoulou D, Pasareanu CS (2003) Learning assumptions for compositional verification. In: Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp 331–346
20. Delzanno G, Podelski A (1999) Model checking in CLP, LNCS 1579:223–239
21. FAST (2004) Fast acceleration of symbolic transition systems. http://www.lsv.ens-cachan.fr/fast/
22. Finkel A, Schnoebelen P (2001) Well-structured transition systems everywhere! Theor Comput Sci 256(1–2):63–92
23. Habermehl P, Vojnar T (2004) Regular model checking using inference of regular languages. In: Proceedings of infinity′04, London, UK
24. Hopcroft JE, Motwani R, Rotwani, Ullman JD (2000) Introduction to automata theory, languages and computability. Addison-Wesley Longman Publishing Co Inc
25. Kearns MJ, Vazirani UV (1994) An introduction to computational learning theory. The MIT Press, Cambridge, Massachusetts
26. Klarlund N, Møller A (2004) Mona. http://www.brics.dk/mona/
27. Kleene S (1952) Introduction to metamathematics. D. van Nostrand, Princeton
28. LASH (2004) The liege automata-based symbolic handler. http://www.montefiore.ulg.ac.be/~boigelot/ research/lash/
29. LEVER (2004) Learning to verify tool. http://www.montefiore.ulg.ac.be/~boigelot/ research/lash/ http://osl.cs.uiuc.edu/ vardhan/lever.html
30. Rivest RL, Schapire RE (1993) Inference of finite automata using homing sequences. Inform Comput 103(2):299–347
31. Rybina T, Voronkov A (2002) Brain: backward reachability analysis with integers. In: AMAST, pp 489–494
32. Tarski A (1955) A lattice-theoretical fixpoint theorem and its applications. Pac J Math 5(2):285–309
34. Vardhan A (2006) Learning to verify systems. PhD thesis, Department of Computer Science, University of Illinois at Urbana Champaign
35. Vardhan A, Sen K, Viswanathan M, Agha G (2004) Actively learning to verify safety for FIFO automata. In: LNCS 3328, Proceedings of FSTTCS′04, Chennai, India, pp 494–505
36. Vardhan A, Sen K, Viswanathan M, Agha G (2004) Learning to verify safety properties. In: LNCS 3308, Proceedings of ICFEM′04, Seattle, USA, pp 274–288
37. Vardhan A, Sen K, Viswanathan M, Agha G (2005) Using language inference to verify omega-regular properties. In: Proceedings of the Eleventh International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS′05), vol 3440, Springer, Edinburgh, UK, pp 45–60