Browsing by Author "Visser, Willem"

Now showing 1 - 5 of 5
  • Thumbnail Image
    Item
    Java Pathfinder at SV-COMP 2019 (Competition Contribution)
    (Springer, 2019) Artho, Cyrille; Visser, Willem
    This paper gives a brief overview of Java Pathfinder, or jpf-core. We describe the architecture of JPF, its strengths, and how it was set up for SV-COMP 2019.
  • Thumbnail Image
    Item
    Model checking rational agents
    (IEEE - -Institute of Electrical and Electronics Engineers, 2004-10) Bordini, Rafael H.; Fisher, Michael; Wooldridge, Michael; Visser, Willem
    Agent-oriented programming techniques seem appropriate for developing systems that operate in complex, dynamic, and unpredictable environments. We aim to address this requirement by developing model-checking techniques for the (automatic or semiautomatic) verification of rational-agent systems written in a logic-based agent-oriented programming language. Typically, developers apply model-checking techniques to abstract models of a system rather than the system implementation. Although this is important for detecting design errors at an early stage, developers might still introduce errors during coding. In contrast, developers can directly apply our model-checking techniques to systems implemented in an agent-oriented programming language, automatically verifying agent systems without the usual gap between design and implementation. We developed our techniques for AgentSpeak, a rational-agent programming language based on the AgentSpeak (L) abstract agent-oriented programming language. AgentSpeak shares many features of the agent-oriented programming paradigm. Similarly, we've developed techniques for automatically translating AgentSpeak programs into the model specification language of existing model-checking systems. In this way, we reduce the problem of verifying that an AgentSpeak system has certain BDI logic properties to a conventional LTL model-checking problem.
  • Thumbnail Image
    Item
    Property-based slicing for agent verification
    (Oxford University Press (OUP), 2009-12) Bordini, Rafael H.; Fisher, Michael; Wooldridge, Michael; Visser, Willem
    Programming languages designed specifically for multi-agent systems represent a new programming paradigm that has gained popularity over recent years, with some multi-agent programming languages being used in increasingly sophisticated applications, often in critical areas. To support this, we have developed a set of tools to allow the use of model-checking techniques in the verification of systems directly implemented in one particular language called AgentSpeak. The success of model checking as a verification technique for large software systems is dependent partly on its use in combination with various state-space reduction techniques, an important example of which is property-based slicing. This article introduces an algorithm for property-based slicing of AgentSpeak multi-agent systems. The algorithm uses literal dependence graphs, as developed for slicing logic programs, and generates a program slice whose state space is stuttering-equivalent to that of the original program; the slicing criterion is a property in a logic with LTL operators and (shallow) BDI modalities. In addition to showing correctness and characterizing the complexity of the slicing algorithm, we apply it to an AgentSpeak program based on autonomous planetary exploration rovers, and we discuss how slicing reduces the model-checking state space. The experiment results show a significant reduction in the state space required for model checking that agent, thus indicating that this approach can have an important impact on the future practicality of agent verification.
  • Thumbnail Image
    Item
    A survey of new trends in symbolic execution for software testing and analysis
    (Springer Verlag, 2009-10) Pasareanu, Corina S.; Visser, Willem
    Symbolic execution is a well-known program analysis technique which represents program inputs with symbolic values instead of concrete, initialized, data and executes the program by manipulating program expressions involving the symbolic values. Symbolic execution has been proposed over three decades ago but recently it has found renewed interest in the research community, due in part to the progress in decision procedures, availability of powerful computers and new algorithmic developments. We provide here a survey of some of the new research trends in sym- bolic execution, with particular emphasis on applications to test generation and program analysis. We first describe an approach that handles complex programming constructs such as input recursive data structures, arrays, as well as multith- reading. Furthermore, we describe recent hybrid techniques that combine concrete and symbolic execution to overcome some of the inherent limitations of symbolic execution, such as handling native code or availability of decision proce- dures for the application domain. We follow with a dis- cussion of techniques that can be used to limit the (possi- bly infinite) number of symbolic configurations that need to be analyzed for the symbolic execution of looping pro- grams. Finally, we give a short survey of interesting new applications, such as predictive testing, invariant inference, program repair, analysis of parallel numerical programs and differential symbolic execution.
  • Thumbnail Image
    Item
    Symbolic pathfinder for SV-COMP (Competition Contribution)
    (Springer, 2019) Noller, Yannic; Pasareanu, Corina S.; Fromherz, Aymeric; Le, Xuan-Bach D.; Visser, Willem
    This paper describes the benchmark entry for Symbolic Pathfinder, a symbolic execution tool for Java bytecode. We give a brief description of the tool and we describe the particular run configuration that was used in the SV-COMP competition. Furthermore, we comment on the competition results and we outline some directions for future work.