Research
Research includes the following projects:
- Improvments within GraalVM
- Software verification and automated bug finding
- SPARQL query containment solver
- Wafl functional programming language design and implementation
- ...
Improvments within GraalVM
GraalVM (https://www.graalvm.org/) is a high-performance JDK distribution designed to accelerate the execution of applications written in Java and other JVM languages along with support for JavaScript, Ruby, Python, and a number of other popular languages. GraalVM’s polyglot capabilities make it possible to mix multiple programming languages in a single application while eliminating foreign language call costs.
Research topics:
- Profile prediction based on machine learning
- Compiler parameter inference based on machine learning
- Metrics for monitoring effects of static analysis within compilers
- Implementing a framework for interpreters that allows efficient and transparent polyglot interoperability between different programming languages
Software verification and automated bug finding
LAV is a software verification tool built on top of the LLVM compiler infrastructure, and available under the UIUC open source license.
LAV combines symbolic execution, SAT encoding of program's behavior and some features of bounded model checking. Namely, single blocks of the code are modelled by first-order logic formulae constructed by symbolic execution, while relationships between blocks are modelled by propositional formulae. Formulae that describe blocks' behavior are combined with correctness conditions for individual commands to produce correctness conditions of the program to be verified. These conditions are passed to a SMT solver covering a suitable combination of theories. There is support for export to linear arithmetic, bit-vector arithmetic, the theory of uninterpreted functions (and Ackermannization, as its alternative), and the theory of arrays. LAV can use the following SMT solvers: Boolector, MathSAT, Yices, and Z3. Our experiments suggest that the presented approach is competitive with related tools, so it can be used as a useful alternative for some sorts of verification tasks.
For more information on what LAV is and what it can do, see the LAV page: http://argo.matf.bg.ac.rs/?content=lav
SPARQL query containment solver
SpeCS is a sound and complete SPARQL query containment solver. The approach reduces the query containment problem to the satisfiability problem in FOL and therefore enables the usage of state of the art SMT solvers (SpeCS uses Z3 solver). It covers the most common SPARQL language constructs (conjunctive and cyclic queries, union, filter, from clauses, blank nodes and projections, bind, subqueries, optional, graph, expressions within select clause, builtin functions, etc.) and reasoning under RDF SCHEMA entailment regime. The containment problem can be considered in both standard and subsumption form. Renaming of projection variables is also supported.
For more information, see SpeCS page: http://argo.matf.bg.ac.rs/?content=specs
Wafl functional programming language design and implementation
Wafl is a strongly typed functional programming language, with implicit type inference. It was initially designed as an experimental application of FP languages in Web development. Today, Wafl is a simple and very fast scripting language, with a simple and efficient interface to databases.
For more infromation, see Wafl page: http://www.matf.bg.ac.rs/~smalkov/wafl