Java PathFinder

swMATH7658MaRDI QIDQ19680FDOQ19680

Author name not available (Why is that?)

Cited In (92)

• Automatic Generation of Test Inputs for Mercury
• Model Checking Software
• Computer Aided Verification
• Two-stage agent program verification
• Loop Invariant Symbolic Execution for Parallel Programs
• Abstract interpretation of microcontroller code: intervals meet congruences
• Runtime Exception Detection in Java Programs Using Symbolic Execution
• Programming Languages and Systems
• Tools and Algorithms for the Construction and Analysis of Systems
• Title not available (Why is that?)
• Title not available (Why is that?)
• TAGED Approximations for Temporal Properties Model-Checking
• Verifying Parallel Algorithms and Programs Using Coloured Petri Nets
• Title not available (Why is that?)
• Interface-based specification and verification of concurrency controllers
• Enhancing Symbolic Execution of Heap-Based Programs with Separation Logic for Test Input Generation
• Title not available (Why is that?)
• Combining Model Checking and Testing
• Model checking Erlang programs -- abstracting recursive function calls
• Dynamic incremental hashing in program model checking
• Towards a Framework for Constraint-Based Test Case Generation
• System-level state equality detection for the formal dynamic verification of legacy distributed applications
• A closer look at software refactoring using symbolic execution
• Syntax-directed model checking of sequential programs
• Efficient SAT-based bounded model checking for software verification
• An Introduction to Test Specification in FQL
• Space-reduction strategies for model checking dynamic software
• Using SPIN to analyse the tree identification phase of the IEEE 1394 high-performance serial bus (FireWire) protocol
• Model checking dynamic memory allocation in operating systems
• Model Checking Software
• Computer Aided Verification
• Computer Aided Verification
• Automated Technology for Verification and Analysis
• Tools and Algorithms for the Construction and Analysis of Systems
• Title not available (Why is that?)
• Beyond contracts for concurrency
• Symbolic computation via program transformation
• Formal Approaches to Software Testing
• Title not available (Why is that?)
• Advances in Computing Science – ASIAN 2003. Progamming Languages and Distributed Computation Programming Languages and Distributed Computation
• Optimistic synchronization-based state-space reduction
• Translation from Adapted UML to Promela for CORBA-Based Applications
• A model checking-based approach for security policy verification of mobile systems
• Symbolic predictive analysis for concurrent programs
• Formal testing for separation assurance
• Title not available (Why is that?)
• Title not available (Why is that?)
• Efficient verification of sequential and concurrent C programs
• Predicate abstraction of ANSI-C programs using SAT
• Title not available (Why is that?)
• Information Reuse for Multi-goal Reachability Analyses
• From NuSMV to SPIN: Experiences with model checking flight guidance systems
• Title not available (Why is that?)
• MAVEN: Modular aspect verification and interference analysis
• Concolic testing in logic programming
• A local approach for temporal model checking of Java bytecode
• Title not available (Why is that?)
• Deadlock and starvation free reentrant readers-writers: a case study combining model checking with theorem proving
• Fundamental Approaches to Software Engineering
• Efficient bounded model checking of heap-manipulating programs using tight field bounds
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Linear temporal logic symbolic model checking
• A dynamic logic for deductive verification of multi-threaded programs
• Model checking RAISE applicative specifications
• On theorem prover-based testing
• Threaded behavior protocols
• Automated Reasoning
• Understanding parameters of deductive verification: an empirical investigation of KeY
• Model Checking Database Applications
• Model checking JAVA programs using JAVA PathFinder
• Software Model Checking: Searching for Computations in the Abstract or the Concrete
• Integration of verification methods for program systems
• On partial state matching
• Verification of Boolean programs with unbounded thread creation
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Collaborative Verification and Testing with Explicit Assumptions
• Title not available (Why is that?)
• Hybrid Systems: Computation and Control
• Machine learning steered symbolic execution framework for complex software code
• An overview of the runtime verification tool Java PathExplorer
• Translating Java for multiple model checkers: The Bandera back-end
• Verifying time partitioning in the DEOS scheduling kernel
• Automating Errors and Conflicts Prognostics and Prevention
• Generating Unit Tests from Formal Proofs
• Verification, Model Checking, and Abstract Interpretation
• Title not available (Why is that?)
• Title not available (Why is that?)

This page was built for software: Java PathFinder