UNA4CAREER
This project has received funding from the European Union’s Horizon 2020 Research and Innovation Programme under the Marie Sklodowska-Curie grant agreement Nยบ 847635.
910398. Formal Analysis and Design of Software Systems, FADoSS
Faculty of Computer Science and Engineering
The Formal Analysis and Design of Software Systems (FADoSS) group focuses on the analysis and implementation of formal techniques for verifying the design of software systems. We are interested in analyzing the theoretical foundations of particular software systems, specification methods, theorem proving, and analysis and generation of code. In fact, because software systems are now essential for our everyday lives through mobile devices, cars, infrastructures, etc. and in strategic areas such as health or transportation, errors in these systems cause enormous personal, environmental, and economic damage. For these reasons, it is critical to ensure that the software used by them is safe and does not consume more resources than it should. FADoSS members have applied a variety of formal techniques to analyze several systems; among the successful analyses performed in the group we find debugging of concurrent systems, application of bio-inspired algorithms to optimization problems, and analysis of blockchain and smart contracts.
Researchers in FADoSS work actively with external researchers, both in Spain and overseas. In particular, we collaborate with researchers from University of Illinois at Urbana-Champaign (USA), SRI International (USA), Philipps-Universität Marburg (Germany), Japan Advanced Institute of Science and Technology (Japan), and University of ReykjavÃk (Iceland), among many others.
The group is located at the School of Computer Science and Engineering, which provides offices for postdoc researchers. Because the group focuses on software-oriented research, we will provide postdoc researchers with a laptop/PC. Most of the software used by the FADoSS group is open-source and freely available, but we also purchase new versions of any required sofware.
Our research topics include:
– Analysis of equivalence via bisimulations, that is, checking whether two transition systems behave in the same way if one simulates the other (and vice versa).
– Formal models for concurrency, like Petri Nets.
– Improvements for the specification language Maude, including execution strategies, new narrowing commands, integration with other tools (e.g. Python and SMTs), compositional definition of specifications, etc.
– Definition of semantics of systems in rewriting logic and application of standard analysis techniques (e.g. model checking) to these systems.
– Analysis of programming languages parameterized by the semantics. That is, defining general analysis techniques that can be later instantiated with the semantics of particular programming langauges, making these techniques easily available to all programs written using these languages.
– New techniques for theorem proving, including new induction schemas (e.g. based in membership axioms), new decision procedures for existing theorem provers, combination with SMT, etc.
– Optimization via bio-inspired algorithms. Algorithms based on the behavior of animals, like ants and birds, provide approximate solutions to complex problems in practice, so they have been used to compute close solutions to problems whose best solution cannot be found in practice.
– Applications of formal methods to new paradigms, like robot design, blockchain, smart contracts, Internet of Things, big data, etc.
– Analysis of complexity of programs.
