TutorialsASE 2023

Powerful graph solver algorithm for the generation and analysis of consistent models.

Nickname: Refinery

Authors: Oszkár Semeráth^*, Kristóf Marussy^* and Dániel Varró^**

Institutions: ^*Budapest University of Technology and ^**Economics and **Linköping University

Duration: 1.5 hour

Abstract: Graph-based models are widely used in software and system engineering. Consequently, several testing, benchmarking, and optimization problem relies on the systematic construction of consistent graph models. However, automatically generating a diverse set of consistent graph models for industrial domains is challenging. First, engineers must specify the graph generation problem with mathematical precision, requiring specialized tools. Second, graph generation is a computationally complex task requiring specialized logic solvers. The Refinery framework is a novel open-source software tool automatically synthesizes consistent and diverse domain-specific graph models. The framework offers an expressive high-level language using partial models to succinctly formulate a wide range of graph generation challenges. Application scenarios include system-level architecture synthesis, test generation for modeling tools or traffic scenario synthesis for autonomous vehicles. The framework uses a scalable graph solver algorithm that uses logic reasoning rules to efficiently synthesize a diverse set of solutions to graph generation problems by combining partial model refinement with logic reasoning. In our tutorial, we present our graph generation tool to the software engineering community and show how to automate various problems with automated graph generation.

Social, Legal, Ethical, Empathetic and Cultural Requirements: from Elicitation to Verification

Nickname: Requirements

Authors: Sinem Getir Yaman^*, Ana Cavalcanti*, Radu Calinescu^*, Beverly Townsend^**

Institutions: ^*Department of Computer Science and ^**Law School, University of York, UK

Duration: 3 hours

Abstract: A new class of requirements is of growing importance for many software systems. In applications ranging from assistive care to emergency management, software systems perform operations and make decisions that must comply with the social, legal, ethical, empathetic and cultural (SLEEC) norms of their users. For example, the control software of an assistive-care robot must consider its users' well-being, privacy and autonomy needs. As another example, a software personal assistant must exhibit cultural sensitivity when addressing its users, and must seek user consent prior to sharing certain types of personal information. In this tutorial, we will present a tool-supported methodology for the elicitation, formalisation, consistency validation, and verification of these SLEEC requirements, using interactive exercises to demonstrate its application to software systems from domains such as assistive care and emergency management.

Collaborative Analysis and Verification of C Programs with Frama-C

Nickname: Frama-C

Authors: Frédéric Loulergue

Institution: University of Orléans, France

Duration: half-day

Abstract: While ensuring the correctness of an implementation based on a formal functional specification provides the strongest guarantee, it can be prohibitively expensive to achieve. In practice, a combination of formal methods is commonly employed to attain an appropriate level of assurance. This includes static analyses to ensure the absence of runtime errors, deductive verification for functional correctness, and dynamic verification for components that cannot be proven through deductive verification. Frama-C is a source code analysis platform designed for the verification of large-scale programs written in ISO C source code. It offers comprehensive support for the integration of formal methods, offering users a set of plug-ins that facilitate static and dynamic analysis of safety-critical and security-critical software. Furthermore, the collaborative verification capabilities are achieved through the integration of these plug-ins on a shared kernel and their adherence to a standardized specification language known as ACSL (ANSI/ISO C Specification Language). This tutorial is an introduction, including hands-on sessions, to the analysis and verification of C programs using Frama-C. The main plug-ins of Frama-C are presented, as well as their combination in a verification project. We illustrate these plug-ins on several examples taken from Contiki, a lightweight operating system for the Internet of Things.

AI for SE

Nickname: AI for SE

Authors: Mohamad Khajezade, Iman Saberi, Fatemeh H. Fard

Institution: University of British Columbia

Duration: 3 hours

Abstract: Recently, many efforts have been made in the Software Engineering community to use language models (LM) such as CodeBERT or large language models (LLM) such as GPT3 to automate and improve the performance of SE tasks. Though fine-tuning the language models or providing a prompt to an LLM is a common way of using these models, the learned knowledge of these models can be transferred to a new language, task, or domain using other techniques such as few-shot learning and adapters. In this tutorial, we aim first to provide background knowledge about what language models are and how they work. Then, we will dive into different classes of few-shot learning and how they can be applied in the context of source code to the LMs when the training data samples are limited to only a few records. Finally, we will cover the theories required to use adapters and provide technical details about how they can transfer knowledge from other tasks and domains to new tasks and domains without fully fine-tuning or pre-training the models from scratch. The tutorial covers these concepts’ theories and practical aspects by providing interactive code on Google Colab. This tutorial provides the required background to use language models for knowledge transfer and better performance for low-resource languages.

Dynamically Analyzing Python Programs with DynaPyt

Nickname: DynaPyt

Authors: Aryaz Eghbali, Michael Pradel

Institution:

Duration: 3 hours (half day)

Abstract: Python is a popular language with applications covering a variety of domains, such as web applications, automation scripts, and especially machine learning and data analysis. Program analysis techniques provide the means to validate correctness, analyze performance, and check security properties. With Python being a dynamic language, performing program analysis at runtime is an obvious choice, as it allows for precisely observing the actual runtime behavior. However, implementing dynamic analyses with traditional approaches requires significant engineering effort. DynaPyt allows for implementing analyses with minimal effort, and provides the ability to not only observe but to also modify executions. For example, DynaPyt can be used to implement a dynamic taint analysis, for runtime verification of API protocols, to build a dynamic call graph, or to detect possibly incorrect program behavior. This tutorial will provide a hands-on introduction into dynamically analyzing Python programs with DynaPyt. We will guide participants through setting up the tool and implementing several program analyses. After the tutorial, participants will be able to build on DynaPyt for their own future research and tool development.

An Introduction to Quantum Software Engineering

Nickname: QuantumSE

Authors: Jianjun Zhao

Institution: Kyushu University

Duration: 1.5 hour

Abstract: Quantum computing has emerged as a disruptive technology with the potential to revolutionize various industries. However, because quantum software is different in nature from classical software, developing software for quantum computers requires a paradigm shift in traditional software engineering approaches. This tutorial addresses the challenges and opportunities in quantum software engineering and explores state-of-the-art methods and techniques. Participants will gain insights into developing reliable and robust quantum software systems, taking into account the unique characteristics of quantum systems. The tutorial fosters collaboration between researchers and practitioners, providing a platform to exchange ideas and experiences in quantum software engineering.

Language-Based Testing

Nickname: Zeller

Authors: Andreas Zeller

Institutions: CISPA

Duration: 1.5 hour

Abstract: Common fuzzing techniques work by systematically mutating a set of given inputs, slowly covering more and more of the program code. But if your program has a complex input format, most of these mutations will be invalid, resulting in very few inputs reaching code beyond input processing. In this tutorial, we will explore techniques to generate input languages using grammars, generators, and constraint solvers and leverage these language specifications to create powerful test generators for complex input formats. On top, we can even use these language specifications to check outputs, addressing the oracle problem. Includes interactive coding!

Recommended reads fuzzingbook.org, notably the chapters “Fuzzing with Grammars”, “Fuzzing with Generators”, and “Fuzzing with Constraints”