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 34 articles , 1 standard article )

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

1 2 next

  1. Bruse, Florian; Kreiker, Jörg; Lange, Martin; Sälzer, Marco: Local higher-order fixpoint iteration (2020)
  2. Lu, Xu; Duan, Zhenhua; Tian, Cong; Du, Hongwei: Verify heaps via unified model checking (2020)
  3. Feldman, Yotam M. Y.; Padon, Oded; Immerman, Neil; Sagiv, Mooly; Shoham, Sharon: Bounded quantifier instantiation for checking inductive invariants (2017)
  4. Li, Huisong; Berenger, Francois; Chang, Bor-Yuh Evan; Rival, Xavier: Semantic-directed clumping of disjunctive abstract states (2017)
  5. Ferrara, Pietro: A generic framework for heap and value analyses of object-oriented programming languages (2016)
  6. Kroening, Daniel; Sharygina, Natasha; Tonetta, Stefano; Tsitovich, Aliaksei; Wintersteiger, Christoph M.: Loop summarization using state and transition invariants (2013)
  7. Brochenin, Rémi; Demri, Stéphane; Lozes, Etienne: On the almighty wand (2012)
  8. Ferrara, Pietro; Müller, Peter: Automatic inference of access permissions (2012)
  9. 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
  10. Cherini, Renato; Rearte, Lucas; Blanco, Javier: A shape analysis for non-linear data structures (2010)
  11. Bansal, Kshitij; Brochenin, Rémi; Lozes, Etienne: Beyond shapes: Lists with ordered data (2009)
  12. Brochenin, Rémi; Demri, Stéphane; Lozes, Etienne: Reasoning about sequences of memory states (2009)
  13. Chatterjee, Shaunak; Lahiri, Shuvendu K.; Qadeer, Shaz; Rakamarić, Zvonimir: A low-level memory model and an accompanying reachability predicate (2009) ioport
  14. Kidd, Nicholas; Reps, Thomas; Dolby, Julian; Vaziri, Mandana: Finding concurrency-related bugs using random isolation (2009)
  15. Berdine, J.; Lev-Ami, T.; Manevich, R.; Ramalingam, G.; Sagiv, M.: Thread quantification for concurrent shape analysis (2008)
  16. Lahiri, Shuvendu; Qadeer, Shaz: Back to the future, revisiting precise program verification using SMT solvers (2008)
  17. Manevich, Roman; Lev-Ami, Tal; Sagiv, Mooly; Ramalingam, Ganesan; Berdine, Josh: Heap decomposition for concurrent shape analysis (2008)
  18. Méndez-Lojo, Mario; Navas, Jorge; Hermenegildo, Manuel V.: A flexible, (C)LP-based approach to the analysis of object-oriented programs (2008)
  19. Yang, Hongseok; Lee, Oukseh; Berdine, Josh; Calcagno, Cristiano; Cook, Byron; Distefano, Dino; O’Hearn, Peter: Scalable shape analysis for systems code (2008)
  20. Berdine, Josh; Calcagno, Cristiano; Cook, Byron; Distefano, Dino; O’Hearn, Peter W.; Wies, Thomas; Yang, Hongseok: Shape analysis for composite data structures (2007)

1 2 next