|
|
Code Assertions Verification Using Backward Symbolic Execution
Husák, Robert ; Kofroň, Jan (advisor) ; Parízek, Pavel (referee)
In order to prevent, detect and fix errors in software, various tools for programmers are available, while some of them are able to reason about the behaviour of the program. In the case of C# programming language, the main representatives are Microsoft FxCop, Code Contracts and Pex. Those tools can, indeed, help to build a highly reliable software. However, when a company wants to include them in the software development process, there is a significant overhead involved. Therefore, we created a "light- weight" assertion verification tool called AskTheCode that can help the user to focus on a particular problem at a time that needs to be solved. Because of its goal-driven approach, we decided to implement it using backward symbolic execution. Although it can currently handle only basic C# statements and data types, the evaluation against the existing tools shows that it has the potential to eventually provide significant added value to the user once developed further. Powered by TCPDF (www.tcpdf.org)
|
|
| |
|
| |
|
| |
|
|
Heuristická redukce paralelismu v prostředí komponenty
Pařízek, P. ; Plášil, František
Code model checking of software components suffers from the well-known problem of state explosion when applied to highly parallel components, despite the fact that a single component typically comprises a smaller state space than the whole system. We present a technique that addresses the problem of state explosion in code checking of primitive components with the Java PathFinder in case the checked property is absence of concurrency errors. The key idea is reduction of parallelism in the environment so that only those parts of the component’s code that can likely cause concurrency errors are exercised in parallel; such parts are identified via a heuristic static code analysis (searching for “suspicious” patterns in the component code). Benefits of the technique, i.e. support for discovery of concurrency errors in limited time and space and provision of easy-to-read counterexamples, are illustrated on the results of several experiments.
|
|
|
Model checking softwarových komponent: úprava Java PathFinder pro spolupráci s Behavior Protocol Checker
Pařízek, P. ; Plášil, František ; Kofroň, Jan
Although there exist several software model checkers that check the code against properties specified e.g. via a temporal logic and assertions, or just verifying low-level properties (like unhandled exceptions), none of them supports checking of software components against a high-level behavior specification. We present our approach to model checking of software components implemented in Java against a high-level specification of their behavior defined via behavior protocols 1 which employs the Java PathFinder model checker and the protocol checker. The property checked by the Java PathFinder (JPF) tool (correctness of particular method call sequences) is validated via its cooperation with the protocol checker. We show that just the publisher/listener pattern claimed to be the key flexibility support of JPF (even though proved very useful for our purpose) was not enough to achieve this kind of checking.
|
|
| |
|
| |
|
| |
|
| |
guest ::
RSS feed.