Write a Blog >>
ICST 2020
Mon 23 - Fri 27 March 2020 Porto, Portugal
Keynotes Sessions

Liana Hadarean (Amazon)

Elvira Albert (UCM)

Franjo Ivančić (Google)

Liana Hadarean

One-click formal methods ( Summary)

Formal methods have been successfully applied in domains such as microprocessor hardware design and aerospace. However, despite 50 years of research and development, we have not seen wide adoption of formal methods for large and complex systems such as web services, industrial automation, or enterprise support software. One of the key difficulties when proving security, safety, and robustness of these systems is the problem of finding the models of system architectures necessary for analysis. Additionally, the size of the potential user community and the business value typically does not justify the creation of scalable and easy-to-use tools for formal verification. With the cloud, much of this has changed. Descriptions of cloud services provide accurate models in the form of computer-readable contracts. These contracts establish and govern how the system behaves and in many cases these models are amenable to formal analysis at scale. Most importantly, since those models are used by a large user community, it is now economically feasible to build the tools needed to verify those models. In this talk, we discuss the trend of constructing practical and scalable cloud-based formal methods at Amazon Web Services and how they can easily be used by customers – sometimes with just one-click.


Liana Hadarean is a Senior Applied Scientist in the Automated Reasoning Group at Amazon Web Services. She is currently working on developing a sound static analyzer for Java code. Before joining Amazon, she worked at Synopsys as one of the developers of the Coverity Static Analysis tool. Liana received her PhD from New York University, where her research focused on Satisfiability Modulo Theories (SMT) and she was one of the developers of the CVC4 SMT solver. Her research interests are in the field of formal methods, static analysis and automated reasoning and applying these techniques at scale.

Elvira Albert

Smart – and also reliable and gas-efficient – Contracts

Smart contracts are a very interesting application domain for validation, verification and optimization techniques since (1) they are relatively small in size, hence the application of these techniques scales well, (2) they are valuable (in the corresponding blockchain cryptocurrency), hence software bugs or inefficiencies can cause economical losses, and (3) they require proving new properties to ensure their reliability and efficiency. This talk overviews the main features of smart contracts and discusses our current work on the verification of gas-related and safety properties whose main goals are to save resources, prevent vulnerabilities and avoid potential attacks.


Elvira Albert is a Professor at the Complutense University of Madrid, Spain. She has many years of experience developing validation and verification tools for checking that a software product meets the given requirements or specifications and it thus fulfills its intended behaviour. Over the past two years, she has been investigating on the extension and application of validation and verification techniques to ensure the reliability and efficiency of smart contracts that run on the Ethereum Virtual Machine. She currently leads a large research group, the COSTA team, made up of eight senior researchers and six PhD students. She is author of around 130 publications in international journals and volumes strongly related to the topics of validation and verification of sequential and concurrent programs. Elvira has been recently appointed as Area Editor for the area of Specification, Analysis and Verification of Systems of the TPLP journal and as program co-chair of the next edition of the International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2020).

Franjo Ivančić

SunDew: Systematic Automated Security Testing

At Google, we have found tens of thousands of security and robustness bugs by fuzzing C and C++ libraries. This talk covers the various aspects of one of the projects working on automated scalable techniques related to fuzzing at Google: how to fuzz, what to fuzz, and how to deal with discovered bugs. First, we present a distributed fuzzing infrastructure that allows us to cooperatively utilize multiple test generation techniques. Then, this talk will describe our FUDGE system for automated fuzz driver generation, which automatically generates fuzz driver candidates for libraries based on existing client code. Running large-scale fuzzing services also causes lots of bugs and vulnerabilities to be reported. This talk describes various techniques to provide feedback to developers to reduce the time a known security bug remains open. Finally, this talk will also highlight challenges and opportunities to incorporate security testing into the general software development workflow.


Franjo Ivančić is a Staff Software Engineer at Google in New York focusing on application security, program analysis and software development productivity tools. He is also an Adjunct Assistant Professor in Computer Science at Columbia University in New York. Prior to joining Google, he was a Senior Researcher at NEC Labs in the Systems Analysis and Verification group in Princeton, NJ. At NEC, he developed a number of static and dynamic program analysis tools based on model checking, abstract interpretation and symbolic execution. Before that, he received a Ph.D. in Computer and Information Science from the University of Pennsylvania in Philadelphia, PA. His dissertation research focused on the modeling and verification of embedded and hybrid systems. Earlier, he received a diploma (Dipl.-Inform.) degree from the Rheinische Friedrich-Wilhelms-University in Bonn, Germany, for my research performed at the Fraunhofer Institute in St. Augustin, Germany. My research there focused on Fuzzy Pattern Recognition, Handwriting Recognition and Machine Learning. Before going to Bonn he went to high school at Quirinus-Gymnasium in his hometown of Neuss, Germany, although he is of Croatian descent.