More Like this

1. Satisfiability Modulo Theories: A Beginner’s Tutorial

   https://doi.org/10.1007/978-3-031-71177-0_31  

   Barrett, Clark; Tinelli, Cesare; Barbosa, Haniel; Niemetz, Aina; Preiner, Mathias; Reynolds, Andrew; Zohar, Yoni (September 2024, Springer Nature Switzerland)

   Platzer, Andre; Rozier, Kristin Yvonne; Pradella, Matteo; Rossi, Matteo (Ed.)

   Abstract Great minds have long dreamed of creating machines that can function as general-purpose problem solvers. Satisfiability modulo theories (SMT) has emerged as one pragmatic realization of this dream, providing significant expressive power and automation. This tutorial is a beginner’s guide to SMT. It includes an overview of SMT and its formal foundations, a catalog of the main theories used in SMT solvers, and illustrations of how to obtain models and proofs. Throughout the tutorial, examples and exercises are provided as hands-on activities for the reader. They can be run using either Python or the SMT-LIB language, using either thecvc5or the Z3 SMT solver. 

   more » « less
2. Learning and Leveraging Conventions in the Design of Haptic Shared Control Paradigms for Steering a Ground Vehicle

   https://doi.org/10.1007/s12555-022-0509-6  

   Izadi, Vahid; Ghasemi, Amir H (October 2023, International Journal of Control, Automation and Systems)

   The main objective of this paper is to establish a framework to study the co-adaptation between humans and automation systems in a haptic shared control framework. We specifically used this framework to design control transfer strategies between humans and automation systems to resolve a conflict when co-steering a semi-automated ground vehicle. The proposed framework contains three main parts. First, we defined a modular structure to separate partner-specific strategies from task-dependent representations and use this structure to learn different co-adaption strategies. In this structure, we assume the human and automation steering commands can be determined by optimizing cost functions. For each agent, the costs are defined as a combination of a set of hand-coded features and vectors of weights. The hand-coded features can be selected to describe task-dependent representations. On the other hand, the weight distributions over these features can be used as a proxy to determine the partner-specific conventions. Second, to leverage the learned co-adaptation strategies, we developed a map connecting different strategies to the outputs of human-automation interactions by employing a collaborative-competitive game concept. Finally, using the map, we designed an adaptable automation system capable of co-adapting to human driver’s strategies. Specifically, we designed an episode-based policy search using the deep deterministic policy gradients technique to determine the optimal weights vector distribution of automation’s cost function. The simulation results demonstrate that the handover strategies designed based on co-adaption between human and automation systems can successfully resolve a conflict and improve the performance of the human automation teaming. 

   more » « less
3. Nudging Students Toward Better Software Engineering Behaviors

   Brown, Chris; Parnin, Chris (January 2021, 3rd International Workshop on Bots in Software Engineering.)

   null (Ed.)

   Student experiences in large undergraduate Computer Science courses are increasingly impacted by automated systems. Bots, or agents of software automation, are useful for efficiently grading and generating feedback. Current efforts at automation in CS education focus on supporting instructional tasks, but do not address student struggles due to poor behaviors, such as procrastination. In this paper, we explore using bots to improve the software engineering behaviors of students using developer recommendation choice architectures, a framework incorporating behavioral science concepts in recommendations to improve the actions of programmers. We implemented this framework in class-bot, a novel system designed to nudge students to make better choices while working on programming assignments. This work presents a preliminary evaluation integrating this tool in an introductory programming course. Our results show that class-bot is beneficial for improving student development behaviors increasing code quality and productivity. 

   more » « less
4. Invariant Signature, Logic Reasoning, and Semantic Natural Language Processing (NLP)-Based Automated Building Code Compliance Checking (I-SNACC) Framework

   https://doi.org/10.36680/j.itcon.2023.001  

   Wu, Jin; Xue, Xiaorui; Zhang, Jiansong (January 2023, Journal of Information Technology in Construction)

   Traditional manual building code compliance checking is costly, time-consuming, and human error-prone. With the adoption of Building Information Modeling (BIM), automation in such a checking process becomes more feasible. However, existing methods still face limited automation when applied to different building codes. To address that, in this paper, the authors proposed a new framework that requires minimal input from users and strives for full automation, namely, the Invariant signature, logic reasoning, and Semantic Natural language processing (NLP)-based Automated building Code compliance Checking (I-SNACC) framework. The authors developed an automated building code compliance checking (ACC) prototype system under this framework and tested it on Chapter 10 of the International Building Codes 2015 (IBC 2015). The system was tested on two real projects and achieved 95.2% precision and 100% recall in non-compliance detection. The experiment showed that the framework is promising in building code compliance checking. Compared to the state-of-the-art methods, the new framework increases the degree of automation and saves manual efforts for finding non-compliance cases. 

   more » « less
5. A Formalization of Core Why3 in Coq

   https://doi.org/10.1145/3632902  

   Cohen, Joshua_M; Johnson-Freyd, Philip (January 2024, Proceedings of the ACM on Programming Languages)

   Intermediate verification languages like Why3 and Boogie have made it much easier to build program verifiers, transforming the process into a logic compilation problem rather than a proof automation one. Why3 in particular implements a rich logic for program specification with polymorphism, algebraic data types, recursive functions and predicates, and inductive predicates; it translates this logic to over a dozen solvers and proof assistants. Accordingly, it serves as a backend for many tools, including Frama-C, EasyCrypt, and GNATProve for Ada SPARK. But how can we be sure that these tools are correct? The alternate foundational approach, taken by tools like VST and CakeML, provides strong guarantees by implementing the entire toolchain in a proof assistant, but these tools are harder to build and cannot directly take advantage of SMT solver automation. As a first step toward enabling automated tools with similar foundational guarantees, we give a formal semantics in Coq for the logic fragment of Why3. We show that our semantics are useful by giving a correct-by-construction natural deduction proof system for this logic, using this proof system to verify parts of Why3’s standard library, and proving sound two of Why3’s transformations used to convert terms and formulas into the simpler logics supported by the backend solvers. 

   more » « less