Research

My research focuses on developing methodologies and tools for efficient code- and model-level probabilistic analysis of software and for the verification and adaptation of software systems both at design- and run- time.

My main interests can be enclosed in four areas: probabilistic software analysis, control theory for software engineering, quantitative verification @runtime, and incremental verification.

Probabilistic Software Analysis

Probabilistic software analysis aims at quantifying the probability of a target event to occur during a program execution. Since 2012 I am working on an a set of approaches exploiting symbolic execution to compute the constraints on the inputs leading to the occurrence of a target event; the solution space for such constraints is then quantified given a probabilistic usage profile, which characterizes each input variable by a probability distribution, over its possible values.

Besides its straightforward applications in program analysis, where it allows evaluating quantitative software properties under uncertain usage profile, this technique has a dramatic impact on a number of fields dealing with imprecise and uncertain data, including probabilistic programming, biology, and finance.

Selected related publications

  1. Borges, M., Filieri, A., d’Amorim, M. and Păsăreanu, C.S. Iterative Distribution-Aware Sampling for Probabilistic Symbolic Execution. Proceedings of the 10th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE, 2015), 866–877, [Acceptance rate 74/291, 25.4%].
    - - -
  2. Borges, M., Filieri, A., d’Amorim, M., Păsăreanu, C.S. and Visser, W. Compositional Solution Space Quantification for Probabilistic Software Analysis. Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI, 2014), 123–132, [Acceptance rate 52/287, 18.1%].
    - -
  3. Luckow, K., Păsăreanu, C.S., Dwyer, M.B., Filieri, A. and Visser, W. Exact and Approximate Probabilistic Symbolic Execution for Nondeterministic Programs. Proceedings of the 29th ACM/IEEE International Conference on Automated Software Engineering (ASE, 2014), 575–586, [Acceptance rate 55/337, 16.3%].
    - -
  4. Filieri, A., Păsăreanu, C.S., Visser, W. and Geldenhuys, J. Statistical Symbolic Execution with Informed Sampling. Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE, 2014), 437–448, [Acceptance rate 61/273, 22%].
    - -
  5. Filieri, A., Păsăreanu, C.S. and Visser, W. Reliability Analysis in Symbolic Pathfinder. Proceedings of the 2013 International Conference on Software Engineering (ICSE, 2013), 622–631, [Acceptance rate 85/461, 18.5%].
    - -

Main collaborators

top

Control Theory for Software Engineering

Self-adaptation mechanisms empower software with the ability of withstanding unpredictable changes in its execution environment and handling uncertain knowledge about it. For example a system may automatically allocate more resources or gracefully degrade secondary functionalities when the incoming workload overcomes the current service capabilities. However, these mechanisms rarely provide formal guarantees about their effectiveness and dependability, limiting their applicability in practice.

Control theory has been concerned for decades with controlling of industrial plants aimed at the achievement of prescribed user goals. The mathematical grounding of control theory allows creating controllers effective and dependable by design, under reasonable assumptions about the environmental phenomena that may affect a system behavior. Despite the conceptual similarities between controlling a plant and adapting software, the application of control theory to self-adaptive systems is very limited, with ad hoc solutions hard to generalize.

A comprehensive theory for the control of software systems would allow the design of more robust software, able to dependably tackle the challenges of providing services to an unpredictable, heterogeneous, and dynamic users, by delegating the complexity of handling changes to mathematically guaranteed techniques.

Selected related publications

  1. Filieri, A., Hoffmann, H. and Maggio, M. Automated Multi-Objective Control for Self-Adaptive Software Design. Proceedings of the 10th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE, 2015), 13–24, [Acceptance rate 74/291, 25.4%].
    - -
  2. Filieri, A. et al. Software Engineering Meets Control Theory. Proceedings of the 10th International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS, 2015), [Acceptance rate 16/55, 29%].
    - -
  3. Filieri, A., Hoffmann, H. and Maggio, M. Automated Design of Self-adaptive Software with Control-theoretical Formal Guarantees. Proceedings of the 36th International Conference on Software Engineering (ICSE, 2014), 299–310, [Acceptance rate 99/495, 20%].
    - - -
  4. Filieri, A., Ghezzi, C., Leva, A. and Maggio, M. Reliability-driven Dynamic Binding via Feedback Control. Proceedings of the 7th International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS, 2012), 43–52, [Acceptance rate 15/50, 30%].
    - -
  5. Filieri, A., Ghezzi, C., Leva, A. and Maggio, M. Self-adaptive Software Meets Control Theory: A Preliminary Approach Supporting Reliability Requirements. Proceedings of the 2011 26th IEEE/ACM International Conference on Automated Software Engineering (ASE, 2011), 283–292, [Acceptance rate 37/252, 14.7%].
    - -

Main collaborators

top

Quantitative Verification @Runtime

Unpredictable changes continuously affect software systems and may have a severe impact on their quality of service, potentially jeopardizing a system’s ability to meet the desired requirements. Changes may occur in critical components of the system, services bought by third parties, clients’ operational profiles, requirements, or deployment environments.

Software models and verification techniques at run time may support automatic reasoning about such changes, detect harmful configurations, and potentially enable appropriate reactions. However, traditional verification techniques and tools may not be simply applied as they are at runtime, since they hardly meet the constraints imposed by on-the-fly analysis, in terms of execution time and memory consumption.

Continuous monitoring, learning, and verification of a running system challenge existing techniques far beyond improving their efficiency: new paradigms are required, specifically thought for runtime use. In this field I introduced the “cook first, warm up later” paradigm, where verification task are split into an heavy design-time preprocessing, to be done once for all, leaving for runtime a simpler residual problem to be completed as soon as new information is gathered. A prompt detection of harmful situations is critical for a prompt reaction, which may improve the dependability of a system and avoid loosing information, and in turn a loss of money.

Selected related publications

  1. Filieri, A., Grunske, L. and Leva, A. Lightweight Adaptive Filtering for Efficient Learning and Updating of Probabilistic Models. Proceedings of the 37th International Conference on Software Engineering (ICSE, May 2015), 200–211, [Acceptance rate 84/452, 18.5%].
    - - -
  2. Filieri, A., Ghezzi, C. and Tamburrelli, G. A formal approach to adaptive software: continuous assurance of non-functional requirements. Formal Aspects of Computing. 24, 2 (2012), 163–186.
    - -
  3. Filieri, A. and Ghezzi, C. Further steps towards efficient runtime verification: Handling probabilistic cost models. Formal Methods in Software Engineering: Rigorous and Agile Approaches (FormSERA, Jun. 2012), 2–8, [Acceptance rate 50%].
    - -
  4. Filieri, A., Ghezzi, C. and Tamburrelli, G. Run-time Efficient Probabilistic Model Checking. Proceedings of the 33rd International Conference on Software Engineering (ICSE, 2011), 341–350, [Acceptance rate 62/441, 14.1%]. ACM SigSoft Distinguished Paper Award
    - -

Main collaborators

top

Syntactic-semantic Incremental Verification

Software continuously evolves over time. Adding or removing features, improving on old algorithms, or connecting to different external services are just a few examples of maintainability changes developers undergo on a daily basis. The spreading of agile methods manifests more than anything else the need for fast iterative development processes to keep the pace of stakeholders’ requests. Unfortunately, verification is a long step behind.

The quality assessment within agile methods is usually limited to testing, mostly for efficiency reasons. Test-driven development is probably the peak of the combination between agile development and the attention to quality. How would the coding change if we would have verification-driven development?

Though only a first step in this direction, incremental verification methods may provide quick feedback to developers, which may get noticed of requirements violation while they are still writing their code. Toward making this utopia reality, we propose a general approach to developing families of verifiers that can support incremental verification for different kinds of artifacts and properties. The proposed syntactic-semantic approach is rooted in operator precedence grammars and their support for incremental parsing. Incremental verification procedures are encoded as attribute grammars, whose incremental evaluation goes hand in hand with incremental parsing.

Selected related publications

  1. Bianculli, D., Filieri, A., Ghezzi, C., Mandrioli, D. and Rizzi, A.M. Syntax-driven Program Verification of Matching Logic Properties. Proceedings of the 3rd FME Workshop on Formal Methods in Software Engineering (FormaliSE, May 2015), 68–74.
    - -
  2. Bianculli, D., Filieri, A., Ghezzi, C. and Mandrioli, D. Syntactic-semantic incrementality for agile verification. Science of Computer Programming. 97, Part 1, (2015), 47–54.
    - -
  3. Bianculli, D., Filieri, A., Ghezzi, C. and Mandrioli, D. Incremental Syntactic-Semantic Reliability Analysis of Evolving Structured Workflows. Leveraging Applications of Formal Methods, Verification and Validation. Technologies for Mastering Change (IS0LA, 2014), 41–55.
    - -
  4. Bianculli, D., Filieri, A., Ghezzi, C. and Mandrioli, D. A Syntactic-Semantic Approach to Incremental Verification. CoRR.
    - -

Main collaborators

top