Research Summary

Marko Dimjašević

October 27, 2015

So far I have worked on several projects, which I briefly outline below.

Compositional Analysis of Android Bluetooth Software Stack.

For my thesis I have been working on analyzing the Bluetooth stack in Android. The main challenge is to verify properties across multiple software layers, which range from applications and their libraries written in Java, down to the operating system and drivers written in C. Therefore, we are looking at ways to learn an interface of each layer and compose this information into a cross-language verification. We rely on our experience and tools in automatic software testing.

Automatic Software Testing.

Thoroughly testing software such that it covers as much of code as possible remains a major challenge. Towards addressing the challenge, we combined dynamic symbolic execution and random testing for automatic software testing in order to be able to reach both deep and hard to reach program states [1,2]. Recently we modularized JDart [3], the dynamic symbolic execution tool we rely on in our approach; a tool paper is under submission.

Malware Detection.

Widespread use of mobile platforms makes them an appealing target for attackers.We developed a technique for automatic analysis and detection of malicious applications [4]. The technique combines automatic software testing, operating system-level interfaces, machine learning, and an insight which models information flow in an application execution. This work is under submission.

Runtime Verification.

The US federal government's project aims to create a new national airspace system that will be able to handle a two to three-fold increase in air traffic. As part of the project, NASA has been developing a software system for air-traffic control. We developed a runtime verification technique [5] for test case generation and verification of such a complex system. This technique greatly improves an old debugging process in NASA that was manual, error-prone, and that did not scale.


Marko Dimjašević.
Automatic testing of software libraries.
In Formal Methods in Computer-Aided Design (FMCAD), 2013.
Extended abstract.

Marko Dimjašević and Zvonimir Rakamarić.
JPF-Doop: Combining concolic and random testing for java.
In Java Pathfinder Workshop (JPF), 2013.
Extended abstract.

Marko Dimjašević, Dimitra Giannakopoulou, Falk Howar, Malte Isberner, Zvonimir Rakamarić, and Vishwanath Raman.
The Dart, the Psyco, and the Doop.
In Proceedings of the Java Pathfinder Workshop (JPF), 2014.

Marko Dimjašević, Simone Atzeni, Ivo Ugrina, and Zvonimir Rakamarić.
Android malware detection based on system calls.
Technical Report UUCS-15-003, University of Utah, School of Computing, 2015.

Marko Dimjašević and Dimitra Giannakopoulou.
Test-case generation for runtime analysis and vice versa: Verification of aircraft separation assurance.
In Proceedings of the International Symposium on Software Testing and Analysis (ISSTA), 2015.