Stack Overflow
Stack Overflow

Questions tagged [jpf]

Java Path Finder (JPF) is a highly customizable execution environment for verification of Java bytecode programs. The system was developed at the US NASA Ames Research Center and released as open source in 2005.

The JPF core is a Virtual Machine for Java bytecode, which means it is a program in which you execute Java programs. It is used to find defects in these programs, so you also need to give it the properties to check for as input. JPF gets back to you with a report that says if the properties hold and/or which verification artifacts have been created by JPF for further analysis (like test cases). JPF offers many features such as symbolic execution, model checking, backtracking, and state matching.

For more information:
http://babelfish.arc.nasa.gov/trac/jpf/wiki/WikiStart

16 questions
5
votes
2 answers

Plugin Management for an Android application

We want to develop and extensible Android application, and are looking for a way to handle plugins. What do you think would be the best approach: Using Android's PackageManager. The problem here is that the PM isn't designed with plugins in mind,…
MasterScrat
  • 7,090
  • 14
  • 48
  • 80
3
votes
2 answers

How to use implementation loaded with different Java classloader?

I am writing a library where I allow people to provide implementations of certain interfaces using a plugin framework (it's JPF if you're familiar). The plugins are not stored in the classpath. The framework gives me a ClassLoader for each plugin,…
Michael Rusch
  • 2,479
  • 2
  • 16
  • 20
3
votes
3 answers

Thread Scheduling - Shared Array

I need two threads to write one a shared array of ints. Both threads need to write on all the elements of that array. Each thread will write either 1 or 7, and the result should be like 171717171 (or 71717171). To do that I have the first Thread1…
Giannis
  • 5,286
  • 15
  • 58
  • 113
2
votes
1 answer

Java Plugin Framework (JPF) and SystemClassLoader

Hello stackoverflow world, I am stuck on a little problem with Java Plugin Framework and I can't find in the documentation an answer to it. The question is surprisingly simple: how to make available from the system class loader the classes brought…
njames
  • 502
  • 1
  • 5
  • 17
1
vote
2 answers

Use Java Path Finder from another java project

I want to use JPF (Java Path Finder) from another java project. Steps that i have done: I have created a new Java project Referenced the jpf-core in build path. Created a java class(Test.java) printing Hello world (in my new project). Created a…
Kishore DVS
  • 51
  • 5
0
votes
1 answer

Run Java path finder

I run java path finder in eclipse and I received the following error: Exception in thread "main" java.lang.SecurityException: Prohibited package name: java.lang at java.lang.ClassLoader.preDefineClass(ClassLoader.java:480) at…
Fiary
  • 203
  • 2
  • 11
0
votes
1 answer

Java Path Finder NumericValueChecker

I am trying to learn Java Path Finder (JPF). I downloaded the JPF and build it. Currently I have jpf-core folder which has example .java files together with their corresponding .jpf files. My goal is to create a new basic .java file and check…
M.Arıcı
  • 37
  • 1
  • 7
0
votes
2 answers

How to run JPF in netbeans.?

I have completed all steps stated below Download and install jpf-core, e.g. from the Mercurial repository -------------- take a break --------------- Download the gov-nasa-jpf-netbeans-runjpf.nbm file from here. From within Netbeans go to…
Sarangan
  • 868
  • 1
  • 8
  • 24
0
votes
2 answers

How to declare Entities on the fly?

I try to develop a Java Plugin application using the Java plugin framework. All plugins will have acces to a uniq database using JPA (with Eclipselink). But each plugin will have there own Entities. So I could not declare all Entities in one unique…
fluminis
  • 3,575
  • 4
  • 34
  • 47
0
votes
1 answer

Not able to run jpf command :JPF exception, terminating: error reading class java.lang.reflect.AnnotatedElement

I am getting the below error when I try to run the jpf basset program. I was able to build jpf-core and jpf-actor successfully. Did anyone encounter this before? Am I missing out something? Appreciate your response/comments. Thanks. …
Zack
  • 2,078
  • 10
  • 33
  • 58
0
votes
1 answer

How to bypass null pointer exception?#JPF

I am trying to run JPF and encountered a following null pointer exception. java.lang.NullPointerException at gov.nasa.jpf.vm.ThreadInfo$StackTraceElement.createJPFStackTraceElement(ThreadInfo.java:1671) The code that is corresponds to is: int…
abhishek Kanodia
  • 19
  • 1
  • 4
0
votes
0 answers

Java Path finder: How to access it through command terminal?

I am new to Java. I have to detect bugs in a java (KLOC) program. For which I am using Java Path finder. I am running it through commandline cmd. Using the command java -jar build/RunJPF.jar C:\Users\xxx\yyy\src\main\java\zzz.jpf I wanted to know,…
abhishek Kanodia
  • 19
  • 1
  • 4
0
votes
1 answer

Setting jpf in eclipse and ClassNotFoundException

I'm trying to make java path finder work with my test examples, using the verify plugin from eclipse doesn't seem to work for some reason, I'm using then run-JPF method. JPF seems to work until I try to use some external class like:…
Pievis
  • 1,954
  • 1
  • 22
  • 42
0
votes
2 answers

Is there a Model Checking software (like Java Path Finder) but for C#?

About this question being off-topic and too opinion-based, I'll try to be more clear. My goal was to undestand if such a tool existed, I was not interested in opinions about what was the best one. At the time I wrote this question I spent…
flagg19
  • 1,782
  • 2
  • 22
  • 27
0
votes
1 answer

how to get the jpf heuristic live count when using Verify API

I am using something like int y = Verify.getIntFromList(intArray); boolean z = Verify.getBoolean(); //do something with y and z i.e. all possible permutations of y and z etc. I am interested in getting the live count of jpf as it go through each…
user2035802
  • 11
  • 3
1
2