Java PathFinder

MaRDI QIDQ19680swMATHFDO

Official website http://javapathfinder.sourceforge.net/

Cited in

(only showing first 100 items - show all)

• Integration of verification methods for program systems
• scientific article; zbMATH DE number 1670550 (Why is no real title available?)
• scientific article; zbMATH DE number 1670561 (Why is no real title available?)
• Linear temporal logic symbolic model checking
• scientific article; zbMATH DE number 1953278 (Why is no real title available?)
• A dynamic logic for deductive verification of multi-threaded programs
• Model checking RAISE applicative specifications
• On theorem prover-based testing
• Threaded behavior protocols
• Using SPIN to analyse the tree identification phase of the IEEE 1394 high-performance serial bus (FireWire) protocol
• A local approach for temporal model checking of Java bytecode
• Automating errors and conflicts prognostics and prevention
• Information reuse for multi-goal reachability analyses
• A model checking-based approach for security policy verification of mobile systems
• Symbolic predictive analysis for concurrent programs
• Formal testing for separation assurance
• scientific article; zbMATH DE number 1693529 (Why is no real title available?)
• Automated Reasoning
• Efficient SAT-based bounded model checking for software verification
• Hybrid Systems: Computation and Control
• From NuSMV to SPIN: Experiences with model checking flight guidance systems
• Machine learning steered symbolic execution framework for complex software code
• Deadlock and starvation free reentrant readers-writers: a case study combining model checking with theorem proving
• scientific article; zbMATH DE number 1744960 (Why is no real title available?)
• Translating Java for multiple model checkers: The Bandera back-end
• Verifying time partitioning in the DEOS scheduling kernel
• scientific article; zbMATH DE number 2182600 (Why is no real title available?)
• Syntax-directed model checking of sequential programs
• Model checking JAVA programs using JAVA PathFinder
• Optimistic synchronization-based state-space reduction
• Advances in Computing Science – ASIAN 2003. Progamming Languages and Distributed Computation Programming Languages and Distributed Computation
• MAVEN: Modular aspect verification and interference analysis
• On partial state matching
• Translation from Adapted UML to Promela for CORBA-Based Applications
• SimGridMC
• Symbiotic 2
• CIL
• jCUTE
• SymDIVINE
• AJPF
• Gwendolen
• Coccinelle
• SPL Conqueror
• AGEDIS
• CRN++
• WPDS++
• scientific article; zbMATH DE number 1670556 (Why is no real title available?)
• Fundamental Approaches to Software Engineering
• scientific article; zbMATH DE number 1863159 (Why is no real title available?)
• Corral
• JaCoCo
• DynAlloy
• QSYM
• VIS
• Automated Technology for Verification and Analysis
• scientific article; zbMATH DE number 2080059 (Why is no real title available?)
• Space-reduction strategies for model checking dynamic software
• Software Model Checking: Searching for Computations in the Abstract or the Concrete
• scientific article; zbMATH DE number 1670563 (Why is no real title available?)
• Formal verification for C program
• Beyond contracts for concurrency
• Symbolic computation via program transformation
• Synchrobench
• Verification of Boolean programs with unbounded thread creation
• scientific article; zbMATH DE number 1617314 (Why is no real title available?)
• An introduction to test specification in FQL
• Efficient verification of sequential and concurrent C programs
• Predicate abstraction of ANSI-C programs using SAT
• Understanding parameters of deductive verification: an empirical investigation of KeY
• scientific article; zbMATH DE number 1746650 (Why is no real title available?)
• Generating Unit Tests from Formal Proofs
• Collaborative verification and testing with explicit assumptions
• scientific article; zbMATH DE number 1701757 (Why is no real title available?)
• Verification, Model Checking, and Abstract Interpretation
• Formal Approaches to Software Testing
• Concolic testing in logic programming
• Model checking dynamic memory allocation in operating systems
• IdentityHashMap
• StarFinder
• A closer look at software refactoring using symbolic execution
• Automatic Generation of Test Inputs for Mercury
• TAGED Approximations for Temporal Properties Model-Checking
• Two-stage agent program verification
• Efficient bounded model checking of heap-manipulating programs using tight field bounds
• Loop invariant symbolic execution for parallel programs
• scientific article; zbMATH DE number 2006479 (Why is no real title available?)
• Runtime Exception Detection in Java Programs Using Symbolic Execution
• Tools and Algorithms for the Construction and Analysis of Systems
• Model Checking Software
• scientific article; zbMATH DE number 2087637 (Why is no real title available?)
• Combining model checking and testing
• scientific article; zbMATH DE number 1973988 (Why is no real title available?)
• scientific article; zbMATH DE number 2146563 (Why is no real title available?)
• Enhancing symbolic execution of heap-based programs with separation logic for test input generation
• scientific article; zbMATH DE number 2086950 (Why is no real title available?)
• Verifying parallel algorithms and programs using coloured Petri nets
• System-level state equality detection for the formal dynamic verification of legacy distributed applications
• Towards a framework for constraint-based test case generation
• scientific article; zbMATH DE number 1982203 (Why is no real title available?)
• Computer Aided Verification

This page was built for software: Java PathFinder