TVLA: A System for Implementing Static Analyses. We present TVLA (Three-Valued-Logic Analyzer). TVLA is a “YACC”-like framework for automatically constructing static-analysis algorithms from an operational semantics, where the operational semantics is specified using logical formulae. TVLA has been implemented in Java and was successfully used to perform shape analysis on programs manipulating linked data structures (singly and doubly linked lists), to prove safety properties of Mobile Ambients, and to verify the partial correctness of several sorting programs.

References in zbMATH (referenced in 27 articles , 1 standard article )

Showing results 1 to 20 of 27.
Sorted by year (citations)

1 2 next

  1. Ferrara, Pietro: A generic framework for heap and value analyses of object-oriented programming languages (2016)
  2. Kroening, Daniel; Sharygina, Natasha; Tonetta, Stefano; Tsitovich, Aliaksei; Wintersteiger, Christoph M.: Loop summarization using state and transition invariants (2013)
  3. Brochenin, Rémi; Demri, Stéphane; Lozes, Etienne: On the almighty wand (2012)
  4. Ferrara, Pietro; Müller, Peter: Automatic inference of access permissions (2012)
  5. Navarro, Angeles; Corbera, Francisco; Asenjo, Rafael; Castillo, Rosa; Zapata, Emilio L.: A data dependence test based on the projection of paths over shape graphs (2012) ioport
  6. Cherini, Renato; Rearte, Lucas; Blanco, Javier: A shape analysis for non-linear data structures (2010)
  7. Brochenin, Rémi; Demri, Stéphane; Lozes, Etienne: Reasoning about sequences of memory states (2009)
  8. Chatterjee, Shaunak; Lahiri, Shuvendu K.; Qadeer, Shaz; Rakamarić, Zvonimir: A low-level memory model and an accompanying reachability predicate (2009) ioport
  9. Kidd, Nicholas; Reps, Thomas; Dolby, Julian; Vaziri, Mandana: Finding concurrency-related bugs using random isolation (2009)
  10. Berdine, J.; Lev-Ami, T.; Manevich, R.; Ramalingam, G.; Sagiv, M.: Thread quantification for concurrent shape analysis (2008)
  11. Lahiri, Shuvendu; Qadeer, Shaz: Back to the future, revisiting precise program verification using SMT solvers (2008)
  12. Manevich, Roman; Lev-Ami, Tal; Sagiv, Mooly; Ramalingam, Ganesan; Berdine, Josh: Heap decomposition for concurrent shape analysis (2008)
  13. Méndez-Lojo, Mario; Navas, Jorge; Hermenegildo, Manuel V.: A flexible, (C)LP-based approach to the analysis of object-oriented programs (2008)
  14. Yang, Hongseok; Lee, Oukseh; Berdine, Josh; Calcagno, Cristiano; Cook, Byron; Distefano, Dino; O’Hearn, Peter: Scalable shape analysis for systems code (2008)
  15. Berdine, Josh; Calcagno, Cristiano; Cook, Byron; Distefano, Dino; O’Hearn, Peter W.; Wies, Thomas; Yang, Hongseok: Shape analysis for composite data structures (2007)
  16. Beyer, Dirk; Henzinger, Thomas A.; Jhala, Ranjit; Majumdar, Rupak: The software model checker blast (2007) ioport
  17. Chatterjee, Shaunak; Lahiri, Shuvendu K.; Qadeer, Shaz; Rakamarić, Zvonimir: A reachability predicate for analyzing low-level software (2007)
  18. Rakamarić, Zvonimir; Bruttomesso, Roberto; Hu, Alan J.; Cimatti, Alessandro: Verifying heap-manipulating programs in an SMT framework (2007)
  19. Arnold, Gilad: Specialized 3-valued logic shape analysis using structure-based refinement and loose embedding (2006)
  20. Iosif, Radu; Dwyer, Matthew B.; Hatcliff, John: Translating Java for multiple model checkers: The Bandera back-end (2005)

1 2 next