Java PathFinder

Model checking JAVA programs using JAVA PathFinder. The paper describes a translator called JAVA PATHFINDER (JPF), which translates from JAVA to PROMELA, the modeling language of the SPIN model checker. JPF translates a given JAVA program into a PROMELA model, which then can be model checked using SPIN. The JAVA program may contain assertions, which are translated into similar assertions in the PROMELA model. The PSIN model checker will then look for deadlocks and violations of any stated assertions. JPF generates a PROMELA model with the same state space characteristics as the JAVA program. Hence, the JAVA program must have a finite and tractable state space. The work should be seen in a broader attempt to make formal methods applicable within NASA’s areas such as space, aviation, and robotics. The work is a continuation of an effort to formally analyze, using SPIN, a multi-threaded operating system for the Deep-Space 1 space craft, and of previous work in applying existing model checkers and theorem provers to real applications.


References in zbMATH (referenced in 123 articles )

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

1 2 3 ... 5 6 7 next

  1. Bu, Lei; Liang, Yongjuan; Xie, Zhunyi; Qian, Hong; Hu, Yi-Qi; Yu, Yang; Chen, Xin; Li, Xuandong: Machine learning steered symbolic execution framework for complex software code (2021)
  2. Ponzio, Pablo; Godio, Ariel; Rosner, Nicolás; Arroyo, Marcelo; Aguirre, Nazareno; Frias, Marcelo F.: Efficient bounded model checking of heap-manipulating programs using tight field bounds (2021)
  3. Pham, Long H.; Le, Quang Loc; Phan, Quoc-Sang; Sun, Jun; Qin, Shengchao: Enhancing symbolic execution of heap-based programs with separation logic for test input generation (2019)
  4. Dennis, Louise A.; Fisher, Michael; Webster, Matt: Two-stage agent program verification (2018)
  5. Godefroid, Patrice; Sen, Koushik: Combining model checking and testing (2018)
  6. Guthmuller, Marion; Corona, Gabriel; Quinson, Martin: System-level state equality detection for the formal dynamic verification of legacy distributed applications (2018)
  7. Knüppel, Alexander; Thüm, Thomas; Pardylla, Carsten Immanuel; Schaefer, Ina: Understanding parameters of deductive verification: an empirical investigation of key (2018)
  8. Lauko, Henrich; Ročkai, Petr; Barnat, Jiří: Symbolic computation via program transformation (2018)
  9. Jančík, Pavel; Kofroň, Jan: On partial state matching (2017)
  10. Mesnard, Fred; Payet, Étienne; Vidal, Germán: Concolic testing in logic programming (2015)
  11. Kádár, István; Hegedűs, Péter; Ferenc, Rudolf: Runtime exception detection in Java programs using symbolic execution (2014)
  12. Szabó, Csaba; Kotul, Maroš; Petruš, Richard: A closer look at software refactoring using symbolic execution (2014)
  13. Beckert, Bernhard; Klebanov, Vladimir: A dynamic logic for deductive verification of multi-threaded programs (2013)
  14. Beyer, Dirk; Holzer, Andreas; Tautschnig, Michael; Veith, Helmut: Information reuse for multi-goal reachability analyses (2013)
  15. Brauer, Jörg; King, Andy; Kowalewski, Stefan: Abstract interpretation of microcontroller code: intervals meet congruences (2013)
  16. Brucker, Achim D.; Wolff, Burkhart: On theorem prover-based testing (2013)
  17. Gligoric, Milos; Majumdar, Rupak: Model checking database applications (2013)
  18. Löwe, Stefan: Cpachecker with explicit-value analysis based on CEGAR and interpolation. (Competition contribution) (2013) ioport
  19. Perna, Juan I.; George, Chris: Model checking RAISE applicative specifications (2013)
  20. Poch, Tomáš; Šerý, Ondřej; Plášil, František; Kofroň, Jan: Threaded behavior protocols (2013)

1 2 3 ... 5 6 7 next