Antonio Filieri

Senior Applied Scientist @AWS
Visiting Associate Professor @Imperial
(he/his/him)

"In God we trust;
all others must bring data"
(W. Edwards Deming)
…or a good proof

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-time and run-time.

My main interests can be enclosed in five areas: privacy and security (@AWS), probabilistic program analysis, control theory for software engineering, quantitative verification, and incremental verification.

My academic research projects are partially funded by: EPSRC, The Royal Society, NCSC, and Imperial College London.

Security and Privacy

Since 2022, I worked with several teams at Amazon to develop static analyses, statistical verification, and automated testing that work at Amazon scale. Some of this work powers CodeGuru Security and Inspector. Other analyses target the verification and validation of memory integrity properties, statistical testing of differential privacy algorithms, and formal methods for cryptographic algorithms.

A (small) part of this work has been published in the papers listed below.

Selected related publications

  1. Hossain, S.B., Filieri, A., Dwyer, M.B., Elbaum, S. and Visser, W. Neural-Based Test Oracle Generation: A Large-scale Evaluation and Lessons Learned. Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE, 2023).
    - - -
  2. Banerjee, S. et al. Compositional Taint Analysis for Enforcing Security and Privacy Policies at Scale. Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE, 2023).
    - -
  3. Christakis, M. et al. Input Splitting for Cloud-Based Static Application Security Testing Platforms. Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE, 2022), 1367–1378.
    - -

Probabilistic Program Analysis

Probabilistic program 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. Luo, Y., Filieri, A. and Zhou, Y. SYMPAIS: SYMbolic Parallel Adaptive Importance Sampling for Probabilistic Program Analysis. Proceedings of the ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE, 2021), 23–28, [Acceptance rate 97/396, 24.5%].
    - - -
  2. Converse, H., Filieri, A., Gopinath, D. and Păsăreanu, C.S. Probabilistic Symbolic Analysis of Neural Networks. 2020 IEEE 31st International Symposium on Software Reliability Engineering (ISSRE) (ISSRE, 2020), 148–159.
    - -
  3. Gerrard, M., Borges, M., Dwyer, M. and Fillieri, A. Conditional Quantitative Program Analysis. IEEE Transactions on Software Engineering. (2020).
    - -
  4. 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%].
    - - -
  5. 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%].
    - -

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. Kotegov, I. and Filieri, A. Towards Coordinated Autoscaling and Application Brownout at the Orchestrator Level. Software Architecture (QUDOS, 2020), 269–274.
    - -
  2. Maggio, M., Papadopoulos, A.V., Filieri, A. and Hoffmann, H. Automated Control of Multiple Software Goals using Multiple Actuators. Proceedings of the 12th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC/FSE, 2017), 373–384, [Acceptance rate 72/295, 24.4%].
    - -
  3. Filieri, A. et al. Control Strategies for Self-Adaptive Software Systems. ACM Trans. Auton. Adapt. Syst. 11, 4 (2017), 24:1–24:31.
    - -
  4. 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%].
    - -
  5. 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%].
    - - -

Main collaborators

top

Quantitative Verification

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. Ji, X. and Filieri, A. Probabilistic Counterexample Guidance for Safer Reinforcement Learning. Quantitative Evaluation of Systems (QEST, 2023), 311–328.
    - -
  2. Wang, R., Casale, G. and Filieri, A. Estimating Multiclass Service Demand Distributions Using Markovian Arrival Processes. ACM Trans. Model. Comput. Simul. 33, 1–2 (Feb. 2023).
    - -
  3. Wang, R., Casale, G. and Filieri, A. Enhancing Performance Modeling of Serverless Functions via Static Analysis. Proceedings of the International Conference on Service-Oriented Computing (ICSOC, 2022), 71–88. Best Paper Award
    - -
  4. Wang, R., Casale, G. and Filieri, A. Service Distribution Estimation for Microservices Using Markovian Arrival Processes. Proceedings of the 18th International Conference on Quantitative Evaluation of SysTems (QEST, 2021), 1–19.
    - -
  5. Filieri, A., Tamburrelli, G. and Ghezzi, C. Supporting Self-adaptation via Quantitative Verification and Sensitivity Analysis at Run Time. IEEE Transactions on Software Engineering. 42, 1 (2016), 75–99.
    - - -

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. Leeson, W., Dwyer, M. and Filieri, A. Sibyl: Improving Software Engineering Tools with SMT Selection. Proceedings of the 45th International Conference on Software Engineering (ICSE, 2023), 2185–2197, [Acceptance rate 209/796, 26%]. ACM Distinguished Paper Award
    - - -
  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., 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, 2015), 68–74.
    - -
  4. 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.
    - -
  5. Bianculli, D., Filieri, A., Ghezzi, C. and Mandrioli, D. A Syntactic-Semantic Approach to Incremental Verification. CoRR.
    - -

Main collaborators

top