Software Verification

Automated Verification of Software

We develop techniques and tools for automated verification of programs that use multiple threads and data containers. A special focus is given to incremental and modular approaches to verification. Most of our techniques are based on predicate abstraction, Craig interpolants, and symbolic execution.

Testing and Debugging Concurrent Programs

The problem of detecting concurrency errors, such as deadlocks and atomicity violations, has become very important especially with greater proliferation of multicore platforms and software that exploits them. We try to design efficient and scalable methods that involve static analysis, dynamic analysis, state space traversal, and randomization. Recently we also started working on tools and techniques for easier debugging of multi-threaded programs.

Analysis of Dynamic Languages

We developed Weverca – a static analysis framework for web applications written in PHP. The aim of the framework is to allow easy specification of precise static analyses. The framework has been used to develop a tool for securing web applications by reporting suspicious code constructs and commands.

... more

Interpolation Techniques

Symbolic techniques and tools (such as SAT and SMT solvers and theorem provers) are used in program verification (establishing interesting properties, such as deadlock absence, race conditions, no assertion violation) to overcome the scaling issues of explicit-state approaches. Some of these methods employ Craig interpolants as an abstract way of representation sets of states. Our research focuses on extendeding this idea to further improve performance of the verification tools in terms of both verification time and consumed memory.

Model-based Testing

In model-based testing, formal specifications are used for testing purposes. In our work, we consider different formal notations: Abstract State Machines, feature models, combinatorial models, NuSMV models, and Boolean expressions. The first field of our research consists in devising abstraction and decomposition techniques for test case generation using model checker and a SAT/SMT solver. Another field of research consists in evaluating the quality of the specifications, and proposing ways to automatically repair them. The third field of research consists in checking that the implementation really reflects its specification by offline testing or runtime verification.

Smart Cyber-Physical Systems

Multi-paradigm modeling of sCPS a IoT

We focus on state-of-the-art methods of model-driven development, requirements-oriented design, and component-based modeling and development. We specifically target large-scale software-intensive cyber-physical systems and aim at developing holistic, multi-paradigm, and well-integrated methods for modeling and developing such systems. This research primarily takes place in the scope of DEECo and IRM projects.

... more

Dynamic and Self-adaptive architectures

As sCPS and IoT need to strike a balance between dependability, open-endedness and adaptability, and operate in dynamic and opportunistic environments, their design and development is challenging and have to integrated self-adaptation. Due to limited connectivity, sCPS typically have to perform adaptation in a decentralized manner, which adds to the overall complexity of designing the adaptation. We focus on designing and developing self-adaptation techniques and methods suitable for sCPS and IoT.

... more

Requirements Processing Methods and Tools

We are working on methods and tools for automated processing requirements written in natural language. Primarily we are focusing on processing textual use-cases.

... more

Performance Modeling

Performance Awareness in Software Development

Software performance tends to be easier to observe after the fact than to design up front. Focusing on the implementation phases of software development, we work on methods that help improve developer awareness of software performance.

... more

Measurement Methodology

Experiments in performance evaluation involve much technical work that must cope with increasingly complex software and hardware stacks to deliver correct results. We publish reusable elements of our experiments to reduce redundant work and help avoid experimental errors.

... more

Dynamic Program Analysis

Dynamic analysis of program behavior helps understand many software properties that are difficult to ascertain from code alone, such as coverage, resource requirements or execution performance. Dynamic program analysis requires flexible monitoring of program execution and efficient processing of collected observations.

... more

Performance Modeling

Performance modeling has many applications in understanding and estimating system performance. We focus on analyzing the effects of sharing low level system resources, such as the processor cores or the memory architecture.

... more

Our Department Is Member of

OW2 Consortium Member SPEC Research Group Member Official Esterel Technologies Academic Partner Google Summer of Code 2014 Mentoring Organization Google Summer of Code 2012 Mentoring Organization Google Summer of Code 2011 Mentoring Organization
Logo of Faculty of Mathematics and Physics
  • Phone: +420 951 554 267, +420 951 554 236
  • Email: info<at-sign>
  • How to find us?
Modified on 2016-03-18