Learning to verify branching time properties

Abhay Vardhan1, Mahesh Viswanathan2
1Google, Inc., Urbana, Illinois
2Dept. of Computer Science, Univ. of Illinois at Urbana-Champaign, Urbana, USA

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/

5. Ammons G, Bodík R, Larus JR (2002) Mining specifications. ACM SIGPLAN Notices 37(1):4–16

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

9. Bartzis C, Bultan T (2004) Widening arithmetic automata. In: Computer aided verification, 2004

10. Berstel J (1979) Transductions and context-free-languages. B.G. Teubner, Stuttgart

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

33. Touili T (2001) Regular model checking using widening techniques. In: ENTCS, vol 50. Elsevier

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

38. Vardhan A, Viswanathan M (2005) Learning to verify branching time properties. In: Proceedings of the twentieth IEEE/ACM International Conference on Automated Software Engineering. Long Beach, California, USA