Write a Blog >>
VenueOakland Center, Michigan, USA
Room nameBallroom C East
Room InformationNo extra information available
Program

You're viewing the program in a time zone which is different from your device's time zone change time zone

Tue 11 Oct

Displayed time zone: Eastern Time (US & Canada) change

10:30 - 12:30
Technical Session 1 - AI for SE IResearch Papers / Industry Showcase at Ballroom C East
Chair(s): Andrea Stocco Università della Svizzera italiana (USI)
10:30
20m
Research paper
B-AIS: An Automated Process for Black-box Evaluation of AI-enabled Software Systems against Domain Semantics
Research Papers
Hamed Barzamini , Mona Rahimi Northern Illinois University
10:50
20m
Industry talk
Automatic Generation of Visualizations for Machine Learning Pipelines
Industry Showcase
Lei Liu Fujitsu Laboratories of America, Inc., Wei-Peng Chen Fujitsu Research of America, Inc., Mehdi Bahrami Fujitsu Laboratories of America, Inc., Mukul Prasad Amazon Web Services
11:10
20m
Research paper
SmOOD: Smoothness-based Out-of-Distribution Detection Approach for Surrogate Neural Networks in Aircraft DesignVirtual
Research Papers
Houssem Ben Braiek École Polytechnique de Montréal, Ali Tfaily Bombardier Aerospace, Foutse Khomh Polytechnique Montréal, Thomas Reid , Ciro Guida Bombardier Aerospace
Pre-print
11:30
20m
Research paper
Unveiling Hidden DNN Defects with Decision-Based Metamorphic TestingVirtual
Research Papers
Yuanyuan Yuan The Hong Kong University of Science and Technology, Qi Pang HKUST, Shuai Wang Hong Kong University of Science and Technology
11:50
20m
Research paper
Patching Weak Convolutional Neural Network Models through Modularization and CompositionVirtual
Research Papers
Binhang Qi Beihang University, Hailong Sun Beihang University, Xiang Gao Beihang University, China, Hongyu Zhang University of Newcastle
12:10
20m
Research paper
Safety and Performance, Why not Both? Bi-Objective Optimized Model Compression toward AI Software DeploymentVirtual
Research Papers
Jie Zhu Peking University, Leye Wang Peking University, Xiao Han Shanghai University of Finance and Economics
DOI Pre-print
14:00 - 15:30
Technical Session 5 - Code AnalysisTool Demonstrations / Research Papers / Journal-first Papers at Ballroom C East
Chair(s): Vahid Alizadeh DePaul University
14:00
20m
Research paper
Detecting Blocking Errors in Go Programs using Localized Abstract InterpretationACM SIGSOFT Distinguished Paper Award
Research Papers
Oskar Haarklou Veileborg Aarhus University, Georgian-Vlad Saioc Aarhus University, Anders Møller Aarhus University
Link to publication
14:20
10m
Demonstration
InvCon: A Dynamic Invariant Detector for Ethereum Smart Contracts
Tool Demonstrations
Ye Liu Nanyang Technological University, Yi Li Nanyang Technological University, Singapore
Pre-print
14:30
20m
Paper
An empirical comparison of four Java-based regression test selection techniques
Journal-first Papers
Min Kyung Shin Colorado State University, Sudipto Ghosh Colorado State University, USA, Leo R. Vijayasarathy Colorado State University
Link to publication DOI
14:50
10m
Demonstration
Augur: Dynamic Taint Analysis for Asynchronous JavaScript
Tool Demonstrations
Mark W. Aldrich Tufts University, Alexi Turcotte Northeastern University, Matthew Blanco Northeastern University, Frank Tip Northeastern University
15:00
10m
Demonstration
FlexType: A Plug-and-Play Framework for Type Inference Models
Tool Demonstrations
Sivani Voruganti UC Davis, Kevin Jesse University of California at Davis, USA, Prem Devanbu Department of Computer Science, University of California, Davis
Pre-print
15:10
20m
Research paper
SelfAPR: Self-supervised Program Repair with Test Execution DiagnosticsVirtual
Research Papers
He Ye KTH Royal Institute of Technology, Matias Martinez Université Polytechnique Hauts-de-France, Xiapu Luo Hong Kong Polytechnic University, Tao Zhang Macau University of Science and Technology (MUST), Martin Monperrus KTH Royal Institute of Technology

Wed 12 Oct

Displayed time zone: Eastern Time (US & Canada) change

10:00 - 12:00
Technical Session 9 - Security and Privacy Research Papers / Industry Showcase at Ballroom C East
Chair(s): Wei Yang University of Texas at Dallas
10:00
20m
Research paper
Keeping Secrets: Multi-objective Genetic Improvement for Detecting and Reducing Information Leakage
Research Papers
Ibrahim Mesecan Iowa State University, Daniel Blackwell University College London, David Clark University College London, Myra Cohen Iowa State University, Justyna Petke University College London
10:20
20m
Research paper
ThirdEye: Attention Maps for Safe Autonomous Driving Systems
Research Papers
Andrea Stocco Università della Svizzera italiana (USI), Paulo J. Nunes Federal University of Pernambuco, Marcelo d'Amorim Federal University of Pernambuco, Paolo Tonella USI Lugano
DOI Pre-print
10:40
20m
Industry talk
Finding Property Violations through Network Falsification: Challenges, Adaptations and Lessons Learned from OpenPilot
Industry Showcase
Meriel von Stein University of Virginia, Sebastian Elbaum University of Virginia
11:00
20m
Research paper
Scrutinizing Privacy Policy Compliance of Virtual Personal Assistant Apps
Research Papers
Fuman Xie University of Queensland, Yanjun Zhang University of Queensland, Chuan Yan University of Queensland, Suwan Li Nanjing University, Lei Bu Nanjing University, Kai Chen SKLOIS, Institute of Information Engineering, Chinese Academy of Sciences, China, Zi Huang University of Queensland, Guangdong Bai University of Queensland
11:20
20m
Research paper
An Empirical Study of Automation in Software Security Patch Management
Research Papers
Nesara Dissanayake University of Adelaide, Asangi Jayatilaka University of Adelaide, Mansooreh Zahedi The Univeristy of Melbourne, Muhammad Ali Babar University of Adelaide
11:40
20m
Research paper
Are They Toeing the Line? Diagnosing Privacy Compliance Violations among Browser Extensions
Research Papers
Yuxi Ling National University of Singapore, Kailong Wang National University of Singapore, Guangdong Bai University of Queensland, Haoyu Wang Huazhong University of Science and Technology, China, Jin Song Dong National University of Singapore
13:30 - 15:30
Technical Session 13 - Application DomainsNIER Track / Research Papers / Journal-first Papers at Ballroom C East
Chair(s): Andrea Stocco Università della Svizzera italiana (USI)
13:30
20m
Research paper
A Hybrid Approach for Inference between Behavioral Exception API Documentation and Implementations, and Its Applications
Research Papers
Hoan Anh Nguyen Amazon, Hung Phan , Samantha Syeda Khairunnesa Bradley University, Son Nguyen The University of Texas at Dallas, Aashish Yadavally University of Texas at Dallas, Shaohua Wang New Jersey Institute of Technology, Hridesh Rajan Iowa State University, Tien N. Nguyen University of Texas at Dallas
13:50
10m
Vision and Emerging Results
Property-Based Automated Repair of DeFi Protocols
NIER Track
Palina Tolmach Nanyang Technological University, Singapore, Institute of High Performance Computing, Agency for Science, Technology and Research (A*STAR), Singapore, Yi Li Nanyang Technological University, Singapore, Shang-Wei Lin Nanyang Technological University
Pre-print
14:00
20m
Research paper
Automatically Detecting Visual Bugs in HTML5 <canvas> Games
Research Papers
Finlay Macklon University of Alberta, Mohammad Reza Taesiri University of Alberta, Markos Viggiato University of Alberta, Stefan Antoszko University of Alberta, Natalia Romanova Prodigy Education, Dale Paas Prodigy Education, Cor-Paul Bezemer University of Alberta
14:20
10m
Vision and Emerging Results
Reflecting on Recurring Failures in IoT Development
NIER Track
Dharun Anandayuvaraj Purdue University, James C. Davis Purdue University, USA
14:30
20m
Research paper
Empirical Study of System Resources Abused by IoT AttackersVirtual
Research Papers
Zijing Yin Tsinghua University, Yiwen Xu Tsinghua University, Chijin Zhou Tsinghua University, Yu Jiang Tsinghua University
14:50
20m
Paper
Large-Scale Empirical Study of Inline Assembly on 7.6 Million Ethereum Smart ContractsVirtual
Journal-first Papers
Xiao Peng China EverBright Bank, Shuwei Song University of Electronic Science and Technology of China, Xiao Peng China EverBright Bank, Xiapu Luo Hong Kong Polytechnic University, Xiao Peng China EverBright Bank, Xiao Peng China EverBright Bank, Ting Chen University of Electronic Science and Technology of China, Jiachi Chen Sun Yat-Sen University, Tao Zhang Macau University of Science and Technology (MUST), Xiaosong Zhang University of Electronic Science and Technology of China
Link to publication DOI
15:10
20m
Research paper
Accelerating OCR-Based Widget Localization for Test Automation of GUI ApplicationsVirtual
Research Papers
Ju Qian Nanjing University of Aeronautics and Astronautics, Yingwei Ma Nanjing University of Aeronautics and Astronautics, Chenghao Lin Nanjing University of Aeronautics and Astronautics, Lin Chen Nanjing University
16:00 - 18:00
Technical Session 19 - Formal Methods and Models IResearch Papers / Journal-first Papers / Tool Demonstrations at Ballroom C East
Chair(s): Michalis Famelis Université de Montréal
16:00
20m
Research paper
Automatic Comment Generation via Multi-Pass Deliberation
Research Papers
Fangwen Mu Institute of Software Chinese Academy of Sciences, Xiao Chen Institute of Software Chinese Academy of Sciences, Lin Shi ISCAS, Song Wang York University, Qing Wang Institute of Software at Chinese Academy of Sciences
16:20
10m
Demonstration
Building recommender systems for modelling languages with DroidVirtual
Tool Demonstrations
Lissette Almonte Universidad Autónoma de Madrid, Esther Guerra Universidad Autónoma de Madrid, Iván Cantador Universidad Autónoma de Madrid, Juan de Lara Autonomous University of Madrid
Pre-print Media Attached
16:30
10m
Demonstration
RobSimVer: A Tool for RoboSim Modeling and AnalysisVirtual
Tool Demonstrations
Dehui Du East China Normal University, Ana Cavalcanti University of York, JihuiNie East China Normal University
16:40
20m
Research paper
Provably Tightest Linear Approximation for Robustness Verification of Sigmoid-like Neural NetworksVirtual
Research Papers
Zhaodi Zhang East China Normal University, Yiting Wu East China Normal University, Si Liu ETH Zurich, Jing Liu East China Normal University, Min Zhang East China Normal University
17:00
20m
Research paper
Efficient Synthesis of Method Call Sequences for Test Generation and Bounded VerificationVirtual
Research Papers
Yunfan Zhang Peking University, Ruidong Zhu Peking University, Yingfei Xiong Peking University, Tao Xie Peking University
17:20
20m
Paper
Demystifying Performance Regressions in String SolversVirtual
Journal-first Papers
Yao Zhang , Xiaofei Xie Singapore Management University, Singapore, Yi Li Nanyang Technological University, Singapore, Yun Lin National University of Singapore, Sen Chen Tianjin University, Yang Liu Nanyang Technological University, Xiaohong Li TianJin University
Link to publication DOI
17:40
20m
Research paper
Detecting Semantic Code Clones by Building AST-based Markov Chains ModelVirtual
Research Papers
Yueming Wu Nanyang Technological University, Siyue Feng Huazhong University of Science and Technology, Deqing Zou Huazhong University of Science and Technology, Hai Jin Huazhong University of Science and Technology

Thu 13 Oct

Displayed time zone: Eastern Time (US & Canada) change

10:00 - 12:00
Technical Session 23 - SecurityTool Demonstrations / Journal-first Papers / Late Breaking Results / Research Papers at Ballroom C East
Chair(s): John-Paul Ore North Carolina State University
10:00
10m
Demonstration
V-Achilles: An Interactive Visualization of Transitive Security Vulnerabilities
Tool Demonstrations
Vipawan Jarukitpipat Mahidol University, Xiao Peng China EverBright Bank, Xiao Peng China EverBright Bank, Chaiyong Ragkhitwetsagul Mahidol University, Thailand, Morakot Choetkiertikul Mahidol University, Thailand, Thanwadee Sunetnanta Mahidol University, Raula Gaikovina Kula Nara Institute of Science and Technology, Bodin Chinthanet Nara Institute of Science and Technology, Takashi Ishio Nara Institute of Science and Technology, Kenichi Matsumoto Nara Institute of Science and Technology
10:10
20m
Paper
Automatic Detection of Java Cryptographic API Misuses: Are We There Yet?
Journal-first Papers
Ying Zhang Virginia Tech, USA, Md Mahir Asef Kabir Virginia Tech, Ya Xiao Virginia Tech, Daphne Yao Virginia Tech, Na Meng Virginia Tech
DOI Pre-print
10:30
10m
Demonstration
A transformer-based IDE plugin for vulnerability detectionVirtual
Tool Demonstrations
Cláudia Mamede FEUP, U.Porto, Eduard Pinconschi FEUP, U.Porto, Rui Abreu Faculty of Engineering, University of Porto, Portugal
10:40
10m
Demonstration
Quacky: Quantitative Access Control Permissiveness Analyzer
Tool Demonstrations
William Eiers University of California at Santa Barbara, USA, Ganesh Sankaran University of California Santa Barbara, Albert Li University of California Santa Barbara, Emily O'Mahony University of California Santa Barbara, Benjamin Prince University of California Santa Barbara, Tevfik Bultan University of California, Santa Barbara
10:50
10m
Paper
Towards Robust Models of Code via Energy-Based Learning on Auxiliary DatasetsVirtual
Late Breaking Results
Nghi D. Q. Bui Singapore Management University, Yijun Yu Huawei Ireland Research Center
11:00
10m
Demonstration
Xscope: Hunting for Cross-Chain Bridge AttacksVirtual
Tool Demonstrations
Jiashuo Zhang Peking University, China, Jianbo Gao Peking University, Yue Li Peking University, Ziming Chen Peking University, Zhi Guan Peking University, Zhong Chen
11:10
20m
Research paper
Reentrancy Vulnerability Detection and Localization: A Deep Learning Based Two-phase ApproachVirtual
Research Papers
Zhuo Zhang Chongqing University, Yan Lei Chongqing University, Meng Yan Chongqing University, Yue Yu College of Computer, National University of Defense Technology, Changsha 410073, China, Jiachi Chen Sun Yat-Sen University, Shangwen Wang National University of Defense Technology, Xiaoguang Mao National University of Defense Technology
13:30 - 15:30
Technical Session 25 - Software RepairsNIER Track / Research Papers / Tool Demonstrations at Ballroom C East
Chair(s): Yannic Noller National University of Singapore
13:30
20m
Research paper
ICEBAR: Feedback-Driven Iterative Repair of Alloy Specifications
Research Papers
Simón Gutiérrez Brida University of Rio Cuarto and CONICET, Argentina, Germán Regis Universidad Nacional de Río Cuarto, Guolong Zheng University of Nebraska Lincoln, Hamid Bagheri University of Nebraska-Lincoln, ThanhVu Nguyen George Mason University, Nazareno Aguirre University of Rio Cuarto and CONICET, Argentina, Marcelo F. Frias Dept. of Software Engineering Instituto Tecnológico de Buenos Aires
13:50
20m
Research paper
Repairing Failure-inducing Inputs with Input Reflection
Research Papers
Yan Xiao National University of Singapore, Yun Lin National University of Singapore, Ivan Beschastnikh University of British Columbia, Changsheng SUN , David Rosenblum George Mason University, Jin Song Dong National University of Singapore
14:10
10m
Demonstration
ElecDaug: Electromagnetic Data Augmentation for Model Repair based on Metamorphic Relation
Tool Demonstrations
Jiawei He , Zhida Bao Harbin Engineering University, Quanjun Zhang Nanjing University, Weisong Sun State Key Laboratory for Novel Software Technology, Nanjing University, Jiawei Liu Nanjing University, Chunrong Fang Nanjing University, Yun Lin National University of Singapore
14:20
20m
Research paper
TransplantFix: Graph Differencing-based Code Transplantation for Automated Program RepairVirtual
Research Papers
Deheng Yang National University of Defense Technology, Xiaoguang Mao National University of Defense Technology, Liqian Chen National University of Defense Technology, China, Xuezheng Xu Academy of Military Sciences, Beijing, China, Yan Lei Chongqing University, David Lo Singapore Management University, Jiayu He National University of Defense Technology, Changsha, China
14:40
10m
Vision and Emerging Results
Multi-objective Optimization-based Bug-fixing Template Mining for Automated Program RepairVirtual
NIER Track
Misoo Kim Sungkyunkwan University, Youngkyoung Kim Sungkyunkwan University, Kicheol Kim SungKyunKwan University, Eunseok Lee Sungkyunkwan University
14:50
20m
Research paper
StandUp4NPR: Standardizing Setup for Empirically Comparing Neural Program Repair SystemsVirtual
Research Papers
Wenkang Zhong State Key Laboratory for Novel Software and Technology, Nanjing University, 22 Hankou Road, Nanjing, China, Hongliang Ge State Key Laboratory for Novel Software and Technology, Nanjing University, 22 Hankou Road, Nanjing, China, Hongfei Ai State Key Laboratory for Novel Software and Technology, Nanjing University, 22 Hankou Road, Nanjing, China, Chuanyi Li State Key Laboratory for Novel Software Technology, Nanjing University, Kui Liu Huawei Software Engineering Application Technology Lab, Jidong Ge , Bin Luo Software Institute, Nanjing University
16:00 - 18:00
Technical Session 29 - AI for SE IIResearch Papers / Journal-first Papers at Ballroom C East
Chair(s): Tim Menzies North Carolina State University
16:00
20m
Research paper
Are Neural Bug Detectors Comparable to Software Developers on Variable Misuse Bugs?
Research Papers
Cedric Richter University of Oldenburg, Jan Haltermann University of Oldenburg, Marie-Christine Jakobs Technical University of Darmstadt, Felix Pauck Paderborn University, Germany, Stefan Schott Paderborn University, Heike Wehrheim University of Oldenburg
DOI Pre-print Media Attached File Attached
16:20
20m
Research paper
Learning Contract Invariants Using Reinforcement Learning
Research Papers
Junrui Liu University of California, Santa Barbara, Yanju Chen University of California at Santa Barbara, Bryan Tan Amazon Web Services, Işıl Dillig University of Texas at Austin, Yu Feng University of California at Santa Barbara
16:40
20m
Research paper
Compressing Pre-trained Models of Code into 3 MB
Research Papers
Jieke Shi Singapore Management University, Zhou Yang Singapore Management University, Bowen Xu School of Information Systems, Singapore Management University, Hong Jin Kang Singapore Management University, Singapore, David Lo Singapore Management University
DOI Pre-print Media Attached
17:00
20m
Research paper
A Transferable Time Series Forecasting Service using Deep Transformer model for Online SystemsVirtual
Research Papers
Tao Huang Tencent, Pengfei Chen Sun Yat-Sen University, Jingrun Zhang School of Data and Computer Science, Sun Yat-sen University, Ruipeng Li Tencent, Rui Wang Tencent
17:20
20m
Paper
The Weights can be Harmful: Pareto Search versus Weighted Search in Multi-Objective Search-Based Software EngineeringVirtual
Journal-first Papers
Tao Chen Loughborough University, Miqing Li University of Birmingham
Pre-print
17:40
20m
Research paper
Robust Learning of Deep Predictive Models from Noisy and Imbalanced Software Engineering DatasetsVirtual
Research Papers
Zhong Li Nanjing, Minxue Pan Nanjing University, Yu Pei Hong Kong Polytechnic University, Tian Zhang Nanjing University, Linzhang Wang Nanjing University, Xuandong Li Nanjing University

Fri 14 Oct

Displayed time zone: Eastern Time (US & Canada) change

08:30 - 10:00
Session 1[Workshop] HILT' 22 at Ballroom C East
  • 830-840 Opening, S. Tucker Taft and Jerome Hugues

  • 840-940 Keynote#1 : Rustan Leino, Senior Principal Engineer, Amazon Web Services

    Title Recent experience with developing formally verified software

    Abstract: Numerous impressive projects have developed formally verified software. Typically, the participants in such projects have been formal-methods experts. Can verification tools also be used by common software engineers? I will reflect on this question in the context of the most recent AWS Encryption SDK, a verified library developed in a team with no particular background in verification. I will also give an overview of the verification-aware programming language Dafny, which was used in this development.

    Bio: K. Rustan M. Leino is a Senior Principal Applied Scientist in the Automated Reasoning Group at Amazon Web Services. Throughout his career, he has developed and applied tools for the formal verification of software. The most recent of these is the Dafny language and verifier, which has been used in projects and education for more than a decade. Leino is an ACM Fellow and a recipient of the CAV Award.


  • 940-1010 Session #1: Formal methods and applications (part 1)
    1. Daniel Larraz (The University of Iowa) and Cesare Tinelli (The University of Iowa).

      Title: Finding Locally Smallest Cut Sets using Max-SMT.

      Abstract: Model-based development (MBD) is increasingly being used for system-level development of safety-critical systems. This approach allows safety engineers to leverage the resultant system model created in the MBD process to assess the system’s resilience to component failure. In particular, one fundamental activity is the identification of minimal cut sets (MCSs), i.e, minimal sets of faults that lead to the violation of a safety requirement. Although the construction of a formal system model enables safety engineers to automate the generation process of MCSs, this is usually a computationally expensive task for complex systems. In this paper, we present a method that leverages Max-SMT solvers to efficiently obtain a small set of faults based on a local optimization of the cut set cardinality. Initial experimental results show the effectiveness of the method in generating cut sets that are close or equal to globally optimal solutions (smallest cut sets) while providing an answer 5.6 times faster on average than the standard method to find a smallest cut set.

08:30
90m
Other
TBA
[Workshop] HILT' 22

10:30 - 12:00
Session 2[Workshop] HILT' 22 at Ballroom C East
  • 1030-1130 Session #1: Formal methods and applications (part 2)
    1. Daniel Larraz (The University of Iowa), Arjun Viswanathan (The University of Iowa), Mickaël Laurent (Université de Paris) and Cesare Tinelli (The University of Iowa).

      Title: Beyond model checking of idealized Lustre in Kind 2.

      Abstract: This paper describes several new features of the open-source model checker Kind 2. Its input language and model checking engines have been extended to allow users to model and reason about systems with machine integers. In addition, Kind 2 can now provide traceability information between specification and design elements, which can be used for several purposes, including assessing the quality of a system specification, tracking the safety impact of model changes, and analyzing the tolerance and resilience of a system against faults or cyber-attacks. Finally, Kind 2 is also able to check whether a component contract is realizable or not, and provide a deadlocking computation and a set of conflicting guarantees when the contract is unrealizable.

    2. Danielle Stewart (University of Minnesota) and John Hatcliff (Kansas State University).

      Title: An AADL Contract Language Supporting Integrated Model- and Code-Level Verification.

      Abstract Model-based systems engineering approaches support the early adoption of a model – a collection of abstractions – of the system under development. The system model can be augmented with key properties of the system including formal specifications of system behavior that codify portions of system and unit-level requirements. There are obvious gaps between the model with formally specified behavior and the deployed system. Previous work on component contract languages has shown how behavior can be specified in models defined using the Architecture Analysis and Design Language (AADL) – a SAE International standard (AS5506C). That work demonstrated the effectiveness of model-level formal methods specification and verification but did not provide a strong and direct connection to system implementations developed using conventional programming languages. In particular, there was no refinement of model-level contracts to programming language-level contracts nor a framework for formally verifying that program code conforms to model-level behavioral specifications. To address these gaps and to enable the practical application of model-contract languages for verification of deployed high-integrity systems, this paper describes the design of GUMBO AADL contract language that integrates and extends key concepts from earlier contract languages. The GUMBO contract language (GCL) is closely aligned to a formal semantics of the AADL run-time framework, which provides a platform- and language-independent specification of AADL semantics. We have enhanced the HAMR AADL code generation framework to translate model-level contracts to programming language-level contracts in the Slang high-integrity language. We demonstrate how the Logika verification tool can automatically verify that Slang-based AADL component implementations conform to contracts, both at the code-level and model-level. Slang-based implementations of AADL systems can be executed directly or compiled to C for deployments on Linux or the seL4 verified microkernel.


  • 1130-1230 Keynote #2: Niko Matsakis, Senior Principal Engineer, Amazon Web Services

    Title: a-mir-formality: a formal model for the Rust language

    Bio: Nicholas Matsakis is a Senior Principal Engineer at AWS and co-lead of the open source Rust language design team. He has worked on Rust since 2011, and led the design of its “secret sauce”, the borrow checker. He has played a number of other roles in Rust over the years, such as being a member of the Rust core team, the lead of the Rust compiler team, and helping to launch the Rust Foundation. Prior to working on Rust, he completed a PhD at ETH Zurich and did his undergraduate study at MIT.

10:30
90m
Other
TBA
[Workshop] HILT' 22

13:30 - 15:00
Session 3[Workshop] HILT' 22 at Ballroom C East
  • 1330-1530 Session #2 : Language and Assurance
    1. David Hardin (Collins Aerospace).

      Title: Hardware/Software Co-Assurance for the Rust Programming Language Applied to Zero Trust Architecture Development.

      Abstract: Zero Trust Architecture requirements are of increasing importance in critical systems development. Zero trust tenets hold that no implicit trust be granted to assets based on their physical or network location. Zero Trust development focuses on authentication, authorization, and shrinking implicit trust zones to the most granular level possible, while maintaining availability and minimizing authentication latency. Performant, high-assurance cryptographic primitives are thus central to successfully realizing a Zero Trust Architecture. The Rust programming language has garnered significant interest and use as a modern, type-safe, memory-safe, and potentially formally analyzable programming language. Our interest in Rust particularly stems from its potential as a hardware/software co-assurance language for developing Zero Trust Architectures. We describe a novel environment enabling Rust to be used as a High-Level Synthesis (HLS) language, suitable for secure and performant Zero Trust application development. Many incumbent HLS languages are a subset of C, and inherit many of the well-known security shortcomings of that language. A Rust-based HLS brings a single modern, type-safe, memory-safe, high-assurance development language for both hardware and software. To study the benefits of this approach, we crafted a Rust HLS subset, and developed a frontend to the hardware/software co-assurance toolchain due to Russinoff and colleagues at Arm, used primarily for floating-point hardware formal verification. This allows us to leverage a number of existing hardware/software co-assurance tools with a minimum investment of time and effort. In this paper, we describe our Rust subset, detail our prototype toolchain, and describe the implementation, performance analysis, formal verification and validation of representative Zero Trust algorithms and data structures written in Rust, emphasizing cryptographic primitives and common data structures.

    2. Claire Dross (AdaCore).

      Title: Containers for Specification in SPARK.

      Abstract: The SPARK tool performs static analysis of Ada programs. It can be used to verify both that a program is free from runtime exceptions and that it conforms to a specification expressed through contracts. To facilitate dynamic analysis, Ada contracts are regular expressions which can be evaluated at execution. As a result, the annotation language of the SPARK tool is restricted to executable constructs. In this context, high-level concepts necessary for specification by contracts need to be supplied as libraries. For example, the latest version of the Ada language introduces unbounded integers and rational numbers to the standard library. In this article, we present the functional containers library which provides collections suitable for use in specification. We explain how they can be used to specify and verify complex programs through concrete examples that have been developed over many years.

    3. S. Tucker Taft (AdaCore).

      Title: Rigorous Pattern Matching as a Language Feature.

      Abstract: Structural pattern-matching as a language feature has become more common in programming languages over the past decade. This paper will consider more generally the challenge of adding pattern matching as a programming language feature, from the points of view of language design, rigorous static error detection, and effectiveness. In this context, a pattern matching language feature can be seen as providing a more rigorous approach to handling the complex conditionals that arise in processing highly structured input

13:30
90m
Other
TBA
[Workshop] HILT' 22

15:30 - 17:00
Session 4[Workshop] HILT' 22 at Ballroom C East
  • 1530-1700 Session #3 : Use Cases
    1. Tabea Bordis (Karlsruhe Institute of Technology), Tobias Runge (Karlsruhe Institute of Technology), Alexander Kittelmann (Karlsruhe Institute of Technology) and Ina Schaefer (Karlsruhe Institute of Technology).

      Title: Correctness-by-Construction: An Overview of the CorC Ecosystem (Short Abstract).

      Abstract: Correctness-by-Construction (CbC) is an incremental software development technique in the field of formal methods to create functionally correct programs guided by a specification. In contrast to post-hoc verification, where the specification and verification takes part after implementing a program, with CbC the specification is defined first, and then the program is successively created using a small set of refinement rules that define side conditions preserving the correctness of the program. This specification-first, refinement-based approach as pursued by CbC has the advantage that errors are likely to be detected earlier in the design process and can be tracked more easily. Even though the idea of CbC emerged over 40 years ago, CbC is not widespread and mostly used to create small algorithms. We believe in the idea of CbC and envision a scaled CbC approach that contributes to solving problems of modern software verification. In this short paper, we give an overview on our research regarding CbC in four different lines of research. For all of them, we provide tool support building the CorC ecosystem that even further enables CbC-based development for different fields of application and size of software systems. Furthermore, we give an outlook on future work that extends on our concepts for CbC.

    2. Laura Humphrey (Air Force Research Laboratory).

      Title: Basic Formal Verification of a Waypoint Manager for Unmanned Air Vehicles in SPARK.

      Abstract: As software becomes more complex, it becomes more difficult to verify its correctness. This poses a particular challenge for autonomous systems, since they are software-intensive and also require strong evidence of correctness in order to be allowed operate in real-world environments. One way to help address this problem is through the use of formal methods, i.e. mathematically-based tools for software and hardware verification. In this paper, we perform formal program verification on a service in OpenUxAS, a free and open source software framework for mission-level, multi-vehicle autonomy. More specifically, we apply the SPARK language and verification toolset to a service that sanity-checks and segments long sequences of vehicle waypoints to prove that it is free of runtime errors.

    3. Howard Ausden (Leidos).

      Title: Getting to 100% availability in a large C++ and Ada program.

      Abstract: Fault tolerance is a key requirement for air traffic control systems. A system failure could lead to hundreds of flights being delayed or cancelled. Using experience from earlier systems a set of techniques were built into our system at inception, including hot standby copies of executables and latest state checkpointed in disk files. As the system matured through formal testing and early site experience additional techniques were added to bolster the MTBF. These include exception safety, runaway process protection, and pro-active monitoring of the system to let us find and fix defects, often without the air traffic controllers being aware. Leidos now has a variety of techniques with defense in depth, and for new developments we scale the number of layers to the difficulty and impact of failure and recovery from the failure. Since Fall 2016, the customer has measured the system as 100% available at all operational sites.


1700 - 1715 Conclusion

15:30
90m
Other
TBA
[Workshop] HILT' 22

Wed 12 Oct

Displayed time zone: Eastern Time (US & Canada) change

Room10:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
Ballroom C East

Thu 13 Oct

Displayed time zone: Eastern Time (US & Canada) change

Room10:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
Ballroom C East

Fri 14 Oct

Displayed time zone: Eastern Time (US & Canada) change

Room8:001530459:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:00153045
Ballroom C East