Showing 1–20 of 20 results for author: Piskac, R

Systematic Use of Random Self-Reducibility against Physical Attacks

Authors: Ferhat Erata, TingHung Chiu, Anthony Etim, Srilalith Nampally, Tejas Raju, Rajashree Ramu, Ruzica Piskac, Timos Antonopoulos, Wenjie Xiong, Jakub Szefer

Abstract: This work presents a novel, black-box software-based countermeasure against physical attacks including power side-channel and fault-injection attacks. The approach uses the concept of random self-reducibility and self-correctness to add randomness and redundancy in the execution for protection. Our approach is at the operation level, is not algorithm-specific, and thus, can be applied for protecti… ▽ More This work presents a novel, black-box software-based countermeasure against physical attacks including power side-channel and fault-injection attacks. The approach uses the concept of random self-reducibility and self-correctness to add randomness and redundancy in the execution for protection. Our approach is at the operation level, is not algorithm-specific, and thus, can be applied for protecting a wide range of algorithms. The countermeasure is empirically evaluated against attacks over operations like modular exponentiation, modular multiplication, polynomial multiplication, and number theoretic transforms. An end-to-end implementation of this countermeasure is demonstrated for RSA-CRT signature algorithm and Kyber Key Generation public key cryptosystems. The countermeasure reduced the power side-channel leakage by two orders of magnitude, to an acceptably secure level in TVLA analysis. For fault injection, the countermeasure reduces the number of faults to 95.4% in average. △ Less

Submitted 8 May, 2024; originally announced May 2024.

Quantum Circuit Reconstruction from Power Side-Channel Attacks on Quantum Computer Controllers

Authors: Ferhat Erata, Chuanqi Xu, Ruzica Piskac, Jakub Szefer

Abstract: The interest in quantum computing has grown rapidly in recent years, and with it grows the importance of securing quantum circuits. A novel type of threat to quantum circuits that dedicated attackers could launch are power trace attacks. To address this threat, this paper presents first formalization and demonstration of using power traces to unlock and steal quantum circuit secrets. With access t… ▽ More The interest in quantum computing has grown rapidly in recent years, and with it grows the importance of securing quantum circuits. A novel type of threat to quantum circuits that dedicated attackers could launch are power trace attacks. To address this threat, this paper presents first formalization and demonstration of using power traces to unlock and steal quantum circuit secrets. With access to power traces, attackers can recover information about the control pulses sent to quantum computers. From the control pulses, the gate level description of the circuits, and eventually the secret algorithms can be reverse engineered. This work demonstrates how and what information could be recovered. This work uses algebraic reconstruction from power traces to realize two new types of single trace attacks: per-channel and total power attacks. The former attack relies on per-channel measurements to perform a brute-force attack to reconstruct the quantum circuits. The latter attack performs a single-trace attack using Mixed-Integer Linear Programming optimization. Through the use of algebraic reconstruction, this work demonstrates that quantum circuit secrets can be stolen with high accuracy. Evaluation on 32 real benchmark quantum circuits shows that our technique is highly effective at reconstructing quantum circuits. The findings not only show the veracity of the potential attacks, but also the need to develop new means to protect quantum circuits from power trace attacks. Throughout this work real control pulse information from real quantum computers is used to demonstrate potential attacks based on simulation of collection of power traces. △ Less

Submitted 28 January, 2024; originally announced January 2024.

Comments: IACR Transactions on Cryptographic Hardware and Embedded Systems

Testing learning-enabled cyber-physical systems with Large-Language Models: A Formal Approach

Authors: Xi Zheng, Aloysius K. Mok, Ruzica Piskac, Yong Jae Lee, Bhaskar Krishnamachari, Dakai Zhu, Oleg Sokolsky, Insup Lee

Abstract: The integration of machine learning (ML) into cyber-physical systems (CPS) offers significant benefits, including enhanced efficiency, predictive capabilities, real-time responsiveness, and the enabling of autonomous operations. This convergence has accelerated the development and deployment of a range of real-world applications, such as autonomous vehicles, delivery drones, service robots, and te… ▽ More The integration of machine learning (ML) into cyber-physical systems (CPS) offers significant benefits, including enhanced efficiency, predictive capabilities, real-time responsiveness, and the enabling of autonomous operations. This convergence has accelerated the development and deployment of a range of real-world applications, such as autonomous vehicles, delivery drones, service robots, and telemedicine procedures. However, the software development life cycle (SDLC) for AI-infused CPS diverges significantly from traditional approaches, featuring data and learning as two critical components. Existing verification and validation techniques are often inadequate for these new paradigms. In this study, we pinpoint the main challenges in ensuring formal safety for learningenabled CPS.We begin by examining testing as the most pragmatic method for verification and validation, summarizing the current state-of-the-art methodologies. Recognizing the limitations in current testing approaches to provide formal safety guarantees, we propose a roadmap to transition from foundational probabilistic testing to a more rigorous approach capable of delivering formal assurance. △ Less

Submitted 16 May, 2024; v1 submitted 13 November, 2023; originally announced November 2023.

Analyzing Intentional Behavior in Autonomous Agents under Uncertainty

Authors: Filip Cano Córdoba, Samuel Judson, Timos Antonopoulos, Katrine Bjørner, Nicholas Shoemaker, Scott J. Shapiro, Ruzica Piskac, Bettina Könighofer

Abstract: Principled accountability for autonomous decision-making in uncertain environments requires distinguishing intentional outcomes from negligent designs from actual accidents. We propose analyzing the behavior of autonomous agents through a quantitative measure of the evidence of intentional behavior. We model an uncertain environment as a Markov Decision Process (MDP). For a given scenario, we rely… ▽ More Principled accountability for autonomous decision-making in uncertain environments requires distinguishing intentional outcomes from negligent designs from actual accidents. We propose analyzing the behavior of autonomous agents through a quantitative measure of the evidence of intentional behavior. We model an uncertain environment as a Markov Decision Process (MDP). For a given scenario, we rely on probabilistic model checking to compute the ability of the agent to influence reaching a certain event. We call this the scope of agency. We say that there is evidence of intentional behavior if the scope of agency is high and the decisions of the agent are close to being optimal for reaching the event. Our method applies counterfactual reasoning to automatically generate relevant scenarios that can be analyzed to increase the confidence of our assessment. In a case study, we show how our method can distinguish between 'intentional' and 'accidental' traffic collisions. △ Less

Submitted 4 July, 2023; originally announced July 2023.

Comments: 10 pages. Accepted for publication at IJCAI 2023 (Main Track)

'Put the Car on the Stand': SMT-based Oracles for Investigating Decisions

Authors: Samuel Judson, Matthew Elacqua, Filip Cano, Timos Antonopoulos, Bettina Könighofer, Scott J. Shapiro, Ruzica Piskac

Abstract: Principled accountability in the aftermath of harms is essential to the trustworthy design and governance of algorithmic decision making. Legal theory offers a paramount method for assessing culpability: putting the agent 'on the stand' to subject their actions and intentions to cross-examination. We show that under minimal assumptions automated reasoning can rigorously interrogate algorithmic beh… ▽ More Principled accountability in the aftermath of harms is essential to the trustworthy design and governance of algorithmic decision making. Legal theory offers a paramount method for assessing culpability: putting the agent 'on the stand' to subject their actions and intentions to cross-examination. We show that under minimal assumptions automated reasoning can rigorously interrogate algorithmic behaviors as in the adversarial process of legal fact finding. We model accountability processes, such as trials or review boards, as Counterfactual-Guided Logic Exploration and Abstraction Refinement (CLEAR) loops. We use the formal methods of symbolic execution and satisfiability modulo theories (SMT) solving to discharge queries about agent behavior in factual and counterfactual scenarios, as adaptively formulated by a human investigator. In order to do so, for a decision algorithm $\mathcal{A}$ we use symbolic execution to represent its logic as a statement $Π$ in the decidable theory $\texttt{QF_FPBV}$. We implement our framework and demonstrate its utility on an illustrative car crash scenario. △ Less

Submitted 29 January, 2024; v1 submitted 9 May, 2023; originally announced May 2023.

Towards Automated Detection of Single-Trace Side-Channel Vulnerabilities in Constant-Time Cryptographic Code

Authors: Ferhat Erata, Ruzica Piskac, Victor Mateu, Jakub Szefer

Abstract: Although cryptographic algorithms may be mathematically secure, it is often possible to leak secret information from the implementation of the algorithms. Timing and power side-channel vulnerabilities are some of the most widely considered threats to cryptographic algorithm implementations. Timing vulnerabilities may be easier to detect and exploit, and all high-quality cryptographic code today sh… ▽ More Although cryptographic algorithms may be mathematically secure, it is often possible to leak secret information from the implementation of the algorithms. Timing and power side-channel vulnerabilities are some of the most widely considered threats to cryptographic algorithm implementations. Timing vulnerabilities may be easier to detect and exploit, and all high-quality cryptographic code today should be written in constant-time style. However, this does not prevent power side-channels from existing. With constant time code, potential attackers can resort to power side-channel attacks to try leaking secrets. Detecting potential power side-channel vulnerabilities is a tedious task, as it requires analyzing code at the assembly level and needs reasoning about which instructions could be leaking information based on their operands and their values. To help make the process of detecting potential power side-channel vulnerabilities easier for cryptographers, this work presents Pascal: Power Analysis Side Channel Attack Locator, a tool that introduces novel symbolic register analysis techniques for binary analysis of constant-time cryptographic algorithms, and verifies locations of potential power side-channel vulnerabilities with high precision. Pascal is evaluated on a number of implementations of post-quantum cryptographic algorithms, and it is able to find dozens of previously reported single-trace power side-channel vulnerabilities in these algorithms, all in an automated manner. △ Less

Submitted 4 April, 2023; originally announced April 2023.

Repairing Bugs in Python Assignments Using Large Language Models

Authors: Jialu Zhang, José Cambronero, Sumit Gulwani, Vu Le, Ruzica Piskac, Gustavo Soares, Gust Verbruggen

Abstract: Students often make mistakes on their introductory programming assignments as part of their learning process. Unfortunately, providing custom repairs for these mistakes can require a substantial amount of time and effort from class instructors. Automated program repair (APR) techniques can be used to synthesize such fixes. Prior work has explored the use of symbolic and neural techniques for APR i… ▽ More Students often make mistakes on their introductory programming assignments as part of their learning process. Unfortunately, providing custom repairs for these mistakes can require a substantial amount of time and effort from class instructors. Automated program repair (APR) techniques can be used to synthesize such fixes. Prior work has explored the use of symbolic and neural techniques for APR in the education domain. Both types of approaches require either substantial engineering efforts or large amounts of data and training. We propose to use a large language model trained on code, such as Codex, to build an APR system -- MMAPR -- for introductory Python programming assignments. Our system can fix both syntactic and semantic mistakes by combining multi-modal prompts, iterative querying, test-case-based selection of few-shots, and program chunking. We evaluate MMAPR on 286 real student programs and compare to a baseline built by combining a state-of-the-art Python syntax repair engine, BIFI, and state-of-the-art Python semantic repair engine for student assignments, Refactory. We find that MMAPR can fix more programs and produce smaller patches on average. △ Less

Submitted 29 September, 2022; originally announced September 2022.

Automated Feedback Generation for Competition-Level Code

Authors: Jialu Zhang, De Li, John C. Kolesar, Hanyuan Shi, Ruzica Piskac

Abstract: Competitive programming has become a popular way for programmers to test their skills. Large-scale online programming contests attract millions of experienced programmers to compete against each other. Competition-level programming problems are challenging in nature, and participants often fail to solve the problem on their first attempt. Some online platforms for competitive programming allow pro… ▽ More Competitive programming has become a popular way for programmers to test their skills. Large-scale online programming contests attract millions of experienced programmers to compete against each other. Competition-level programming problems are challenging in nature, and participants often fail to solve the problem on their first attempt. Some online platforms for competitive programming allow programmers to practice on competition-level problems as well, and the standard feedback for an incorrect practice submission is the first test case that the submission fails. Often, the failed test case does not provide programmers with enough information to resolve the errors in their code, and they abandon the problem after several more unsuccessful attempts. We present Clef, the first data-driven tool that can generate feedback on competition-level code automatically by repairing programmers' incorrect submissions. The key development is that Clef can learn how to generate repairs for incorrect submissions by examining the repairs that other programmers made to their own submissions over time. Since the differences between an incorrect program and a correct program for the same task may be significant, we introduce a new data structure, merge trees, to capture the changes between submissions. Merge trees are versatile: they can encode both large algorithm-level redesigns and small statement-level alterations. Clef applies the patterns it learns from a database of submissions to generate repairs for new submissions outside the database. We evaluated Clef on six real-world problems from Codeforces, the world's largest platform for competitive programming. Clef achieves 42.1% accuracy in repairing programmers' incorrect submissions. Even when given incorrect submissions from programmers who never found the solution to a problem on their own, Clef repairs the users' programs 34.1% of the time. △ Less

Submitted 3 June, 2022; originally announced June 2022.

IVeri: Privacy-Preserving Interdomain Verification

Authors: Ning Luo, Qiao Xiang, Timos Antonopoulos, Ruzica Piskac, Y. Richard Yang, Franck Le

Abstract: In an interdomain network, autonomous systems (ASes) often establish peering agreements, so that one AS (agreement consumer) can influence the routing policies of the other AS (agreement provider). Peering agreements are implemented in the BGP configuration of the agreement provider. It is crucial to verify their implementation because one error can lead to disastrous consequences. However, the fu… ▽ More In an interdomain network, autonomous systems (ASes) often establish peering agreements, so that one AS (agreement consumer) can influence the routing policies of the other AS (agreement provider). Peering agreements are implemented in the BGP configuration of the agreement provider. It is crucial to verify their implementation because one error can lead to disastrous consequences. However, the fundamental challenge for peering agreement verification is how to preserve the privacy of both ASes involved in the agreement. To this end, this paper presents IVeri, the first privacy-preserving interdomain agreement verification system. IVeri models the interdomain agreement verification problem as a SAT formula, and develops a novel, efficient, privacy-serving SAT solver, which uses oblivious shuffling and garbled circuits as the key building blocks to let the agreement consumer and provider collaboratively verify the implementation of interdomain peering agreements without exposing their private information. A prototype of IVeri is implemented and evaluated extensively. Results show that IVeri achieves accurate, privacy-preserving interdomain agreement verification with reasonable overhead. △ Less

Submitted 6 February, 2022; originally announced February 2022.

ETAP: Energy-aware Timing Analysis of Intermittent Programs

Authors: Ferhat Erata, Arda Goknil, Eren Yıldız, Kasım Sinan Yıldırım, Ruzica Piskac, Jakub Szefer, Gökçin Sezgin

Abstract: Energy harvesting battery-free embedded devices rely only on ambient energy harvesting that enables stand-alone and sustainable IoT applications. These devices execute programs when the harvested ambient energy in their energy reservoir is sufficient to operate and stop execution abruptly (and start charging) otherwise. These intermittent programs have varying timing behavior under different energ… ▽ More Energy harvesting battery-free embedded devices rely only on ambient energy harvesting that enables stand-alone and sustainable IoT applications. These devices execute programs when the harvested ambient energy in their energy reservoir is sufficient to operate and stop execution abruptly (and start charging) otherwise. These intermittent programs have varying timing behavior under different energy conditions, hardware configurations, and program structures. This paper presents Energy-aware Timing Analysis of intermittent Programs (ETAP), a probabilistic symbolic execution approach that analyzes the timing and energy behavior of intermittent programs at compile time. ETAP symbolically executes the given program while taking time and energy cost models for ambient energy and dynamic energy consumption into account. We evaluated ETAP on several intermittent programs and compared the compile-time analysis results with executions on real hardware. The results show that ETAP's normalized prediction accuracy is 99.5%, and it speeds up the timing analysis by at least two orders of magnitude compared to manual testing. △ Less

Submitted 3 February, 2022; v1 submitted 27 January, 2022; originally announced January 2022.

Comments: Corrected typos in the previous submission

Can Pre-trained Language Models be Used to Resolve Textual and Semantic Merge Conflicts?

Authors: Jialu Zhang, Todd Mytkowicz, Mike Kaufman, Ruzica Piskac, Shuvendu K. Lahiri

Abstract: Program merging is standard practice when developers integrate their individual changes to a common code base. When the merge algorithm fails, this is called a merge conflict. The conflict either manifests in textual merge conflicts where the merge fails to produce code, or semantic merge conflicts where the merged code results in compiler or test breaks. Resolving these conflicts for large code p… ▽ More Program merging is standard practice when developers integrate their individual changes to a common code base. When the merge algorithm fails, this is called a merge conflict. The conflict either manifests in textual merge conflicts where the merge fails to produce code, or semantic merge conflicts where the merged code results in compiler or test breaks. Resolving these conflicts for large code projects is expensive because it requires developers to manually identify the sources of conflict and correct them. In this paper, we explore the feasibility of automatically repairing merge conflicts (both textual and semantic) using k-shot learning with large neural language models (LM) such as GPT-3. One of the challenges in leveraging such language models is to fit the examples and the queries within a small prompt (2048 tokens). We evaluate LMs and k-shot learning for two broad applications: (a) textual and semantic merge conflicts for a divergent fork Microsoft Edge, and (b) textual merge conflicts for a large number of JavaScript projects in GitHub. Our results are mixed: one one-hand, LMs provide the state-of-the-art (SOTA) performance on semantic merge conflict resolution for Edge compared to earlier symbolic approaches; on the other hand, LMs do not yet obviate the benefits of fine-tuning neural models (when sufficient data is available) or the design of special purpose domain-specific languages (DSL) for restricted patterns for program synthesis. △ Less

Submitted 23 November, 2021; originally announced November 2021.

Succinct Explanations With Cascading Decision Trees

Authors: Jialu Zhang, Yitan Wang, Mark Santolucito, Ruzica Piskac

Abstract: The decision tree is one of the most popular and classical machine learning models from the 1980s. However, in many practical applications, decision trees tend to generate decision paths with excessive depth. Long decision paths often cause overfitting problems, and make models difficult to interpret. With longer decision paths, inference is also more likely to fail when the data contain missing v… ▽ More The decision tree is one of the most popular and classical machine learning models from the 1980s. However, in many practical applications, decision trees tend to generate decision paths with excessive depth. Long decision paths often cause overfitting problems, and make models difficult to interpret. With longer decision paths, inference is also more likely to fail when the data contain missing values. In this work, we propose a new tree model called Cascading Decision Trees to alleviate this problem. The key insight of Cascading Decision Trees is to separate the decision path and the explanation path. Our experiments show that on average, Cascading Decision Trees generate 63.38% shorter explanation paths, avoiding overfitting and thus achieve higher test accuracy. We also empirically demonstrate that Cascading Decision Trees have advantages in the robustness against missing values. △ Less

Submitted 29 November, 2022; v1 submitted 13 October, 2020; originally announced October 2020.

Grammar Filtering For Syntax-Guided Synthesis

Authors: Kairo Morton, William Hallahan, Elven Shum, Ruzica Piskac, Mark Santolucito

Abstract: Programming-by-example (PBE) is a synthesis paradigm that allows users to generate functions by simply providing input-output examples. While a promising interaction paradigm, synthesis is still too slow for realtime interaction and more widespread adoption. Existing approaches to PBE synthesis have used automated reasoning tools, such as SMT solvers, as well as works applying machine learning tec… ▽ More Programming-by-example (PBE) is a synthesis paradigm that allows users to generate functions by simply providing input-output examples. While a promising interaction paradigm, synthesis is still too slow for realtime interaction and more widespread adoption. Existing approaches to PBE synthesis have used automated reasoning tools, such as SMT solvers, as well as works applying machine learning techniques. At its core, the automated reasoning approach relies on highly domain specific knowledge of programming languages. On the other hand, the machine learning approaches utilize the fact that when working with program code, it is possible to generate arbitrarily large training datasets. In this work, we propose a system for using machine learning in tandem with automated reasoning techniques to solve Syntax Guided Synthesis (SyGuS) style PBE problems. By preprocessing SyGuS PBE problems with a neural network, we can use a data driven approach to reduce the size of the search space, then allow automated reasoning-based solvers to more quickly find a solution analytically. Our system is able to run atop existing SyGuS PBE synthesis tools, decreasing the runtime of the winner of the 2019 SyGuS Competition for the PBE Strings track by 47.65% to outperform all of the competing tools. △ Less

Submitted 7 February, 2020; originally announced February 2020.

Synthesizing Functional Reactive Programs

Authors: Bernd Finkbeiner, Felix Klein, Ruzica Piskac, Mark Santolucito

Abstract: Functional Reactive Programming (FRP) is a paradigm that has simplified the construction of reactive programs. There are many libraries that implement incarnations of FRP, using abstractions such as Applicative, Monads, and Arrows. However, finding a good control flow, that correctly manages state and switches behaviors at the right times, still poses a major challenge to developers. An attractive… ▽ More Functional Reactive Programming (FRP) is a paradigm that has simplified the construction of reactive programs. There are many libraries that implement incarnations of FRP, using abstractions such as Applicative, Monads, and Arrows. However, finding a good control flow, that correctly manages state and switches behaviors at the right times, still poses a major challenge to developers. An attractive alternative is specifying the behavior instead of programming it, as made possible by the recently developed logic: Temporal Stream Logic (TSL). However, it has not been explored so far how Control Flow Models (CFMs), as synthesized from TSL specifications, can be turned into executable code that is compatible with libraries building on FRP. We bridge this gap, by showing that CFMs are indeed a suitable formalism to be turned into Applicative, Monadic, and Arrowized FRP. We demonstrate the effectiveness of our translations on a real-world kitchen timer application, which we translate to a desktop application using the Arrowized FRP library Yampa, a web application using the Monadic threepenny-gui library, and to hardware using the Applicative hardware description language ClaSH. △ Less

Submitted 23 May, 2019; originally announced May 2019.

Comments: arXiv admin note: text overlap with arXiv:1712.00246

Identifying Maximal Non-Redundant Integer Cone Generators

Authors: Slobodan Mitrović, Ruzica Piskac, Viktor Kunčak

Abstract: A non-redundant integer cone generator (NICG) of dimension $d$ is a set $S$ of vectors from $\{0,1\}^d$ whose vector sum cannot be generated as a positive integer linear combination of a proper subset of $S$. The largest possible cardinality of NICG of a dimension $d$, denoted by $N(d)$, provides an upper bound on the sparsity of systems of integer equations with a large number of integer variable… ▽ More A non-redundant integer cone generator (NICG) of dimension $d$ is a set $S$ of vectors from $\{0,1\}^d$ whose vector sum cannot be generated as a positive integer linear combination of a proper subset of $S$. The largest possible cardinality of NICG of a dimension $d$, denoted by $N(d)$, provides an upper bound on the sparsity of systems of integer equations with a large number of integer variables. A better estimate of $N(d)$ means that we can consider smaller sub-systems of integer equations when solving systems with many integer variables. Furthermore, given that we can reduce constraints on set algebra expressions to constraints on cardinalities of Venn regions, tighter upper bound on $N(d)$ yields a more efficient decision procedure for a logic of sets with cardinality constraints (BAPA), which has been applied in software verification. Previous attempts to compute $N(d)$ using SAT solvers have not succeeded even for $d=3$. The only known values were computed manually: $N(d)=d$ for $d < 4$ and $N(4) > 4$. We provide the first exact values for $d > 3$, namely, $N(4)=5$, $N(5)=7$, and $N(6)=9$, which is a significant improvement of the known asymptotic bound (which would give only e.g. $N(6) \le 29$, making a decision procedure impractical for $d=6$). We also give lower bounds for $N(7)$, $N(8)$, $N(9)$, and $N(10)$, which are: $11$, $13$, $14$, and $16$, respectively. We describe increasingly sophisticated specialized search algorithms that we used to explore the space of non-redundant generators and obtain these results. △ Less

Submitted 20 March, 2019; originally announced March 2019.

Statically Verifying Continuous Integration Configurations

Authors: Mark Santolucito, Jialu Zhang, Ennan Zhai, Ruzica Piskac

Abstract: Continuous Integration (CI) testing is a popular software development technique that allows developers to easily check that their code can build successfully and pass tests across various system environments. In order to use a CI platform, a developer must include a set of configuration files to a code repository for specifying build conditions. Incorrect configuration settings lead to CI build fa… ▽ More Continuous Integration (CI) testing is a popular software development technique that allows developers to easily check that their code can build successfully and pass tests across various system environments. In order to use a CI platform, a developer must include a set of configuration files to a code repository for specifying build conditions. Incorrect configuration settings lead to CI build failures, which can take hours to run, wasting valuable developer time and delaying product release dates. Debugging CI configurations is challenging because users must manage configurations for the build across many system environments, to which they may not have local access. Thus, the only way to check a CI configuration is to push a commit and wait for the build result. To address this problem, we present the first approach, VeriCI, for statically checking for errors in a given CI configuration before the developer pushes a commit to build on the CI server. Our key insight is that the repositories in a CI environment contain lists of build histories which offer the time-aware repository build status. Driven by this insight, we introduce the Misclassification Guided Abstraction Refinement (MiGAR) loop that automates part of the learning process across the heterogeneous build environments in CI. We then use decision tree learning to generate constraints on the CI configuration that must hold for a build to succeed by training on a large history of continuous integration repository build results. We evaluate VeriCI on real-world data from GitHub and find that we have 83% accuracy of predicting a build failure. △ Less

Submitted 11 May, 2018; originally announced May 2018.

Vehicle Platooning Simulations with Functional Reactive Programming

Authors: Bernd Finkbeiner, Felix Klein, Ruzica Piskac, Mark Santolucito

Abstract: Functional languages have provided major benefits to the verification community. Although features such as purity, a strong type system, and computational abstractions can help guide programmers away from costly errors, these can present challenges when used in a reactive system. Functional Reactive Programming is a paradigm that allows users the benefits of functional languages and an easy interf… ▽ More Functional languages have provided major benefits to the verification community. Although features such as purity, a strong type system, and computational abstractions can help guide programmers away from costly errors, these can present challenges when used in a reactive system. Functional Reactive Programming is a paradigm that allows users the benefits of functional languages and an easy interface to a reactive environment. We present a tool for building autonomous vehicle controllers in FRP using Haskell. △ Less

Submitted 27 March, 2018; originally announced March 2018.

Comments: SCAV@CPSWeek 2017

Temporal Stream Logic: Synthesis beyond the Bools

Authors: Bernd Finkbeiner, Felix Klein, Ruzica Piskac, Mark Santolucito

Abstract: Reactive systems that operate in environments with complex data, such as mobile apps or embedded controllers with many sensors, are difficult to synthesize. Synthesis tools usually fail for such systems because the state space resulting from the discretization of the data is too large. We introduce TSL, a new temporal logic that separates control and data. We provide a CEGAR-based synthesis approa… ▽ More Reactive systems that operate in environments with complex data, such as mobile apps or embedded controllers with many sensors, are difficult to synthesize. Synthesis tools usually fail for such systems because the state space resulting from the discretization of the data is too large. We introduce TSL, a new temporal logic that separates control and data. We provide a CEGAR-based synthesis approach for the construction of implementations that are guaranteed to satisfy a TSL specification for all possible instantiations of the data processing functions. TSL provides an attractive trade-off for synthesis. On the one hand, synthesis from TSL, unlike synthesis from standard temporal logics, is undecidable in general. On the other hand, however, synthesis from TSL is scalable, because it is independent of the complexity of the handled data. Among other benchmarks, we have successfully synthesized a music player Android app and a controller for an autonomous vehicle in the Open Race Car Simulator (TORCS.) △ Less

Submitted 8 May, 2019; v1 submitted 1 December, 2017; originally announced December 2017.

Proceedings Fifth Workshop on Synthesis

Authors: Ruzica Piskac, Rayna Dimitrova

Abstract: The SYNT workshop aims to bring together researchers interested in the broad area of synthesis of computing systems. The goal is to foster the development of frontier techniques in automating the development of computing system. Contributions of interest include algorithms, complexity and decidability analysis, as well as reproducible heuristics, implemented tools, and experimental evaluation. Ap… ▽ More The SYNT workshop aims to bring together researchers interested in the broad area of synthesis of computing systems. The goal is to foster the development of frontier techniques in automating the development of computing system. Contributions of interest include algorithms, complexity and decidability analysis, as well as reproducible heuristics, implemented tools, and experimental evaluation. Application domains include software, hardware, embedded, and cyberphysical systems. Computation models include functional, reactive, hybrid and timed systems. Identifying, formalizing, and evaluating synthesis in particular application domains is encouraged. The fifth iteration of the workshop took place in Toronto, Canada. It was co-located with the 28th International Conference on Computer Aided Verification. The workshop included twelve contributed talks and two invited talks. In addition, it featured a special session about the Syntax-Guided Synthesis Competition (SyGuS) and the SyntComp Synthesis competition. △ Less

Submitted 22 November, 2016; originally announced November 2016.

Journal ref: EPTCS 229, 2016

Incremental, Inductive Coverability

Authors: Johannes Kloos, Rupak Majumdar, Filip Niksic, Ruzica Piskac

Abstract: We give an incremental, inductive (IC3) procedure to check coverability of well-structured transition systems. Our procedure generalizes the IC3 procedure for safety verification that has been successfully applied in finite-state hardware verification to infinite-state well-structured transition systems. We show that our procedure is sound, complete, and terminating for downward-finite well-struct… ▽ More We give an incremental, inductive (IC3) procedure to check coverability of well-structured transition systems. Our procedure generalizes the IC3 procedure for safety verification that has been successfully applied in finite-state hardware verification to infinite-state well-structured transition systems. We show that our procedure is sound, complete, and terminating for downward-finite well-structured transition systems---where each state has a finite number of states below it---a class that contains extensions of Petri nets, broadcast protocols, and lossy channel systems. We have implemented our algorithm for checking coverability of Petri nets. We describe how the algorithm can be efficiently implemented without the use of SMT solvers. Our experiments on standard Petri net benchmarks show that IC3 is competitive with state-of-the-art implementations for coverability based on symbolic backward analysis or expand-enlarge-and-check algorithms both in time taken and space usage. △ Less

Submitted 22 February, 2013; v1 submitted 30 January, 2013; originally announced January 2013.

Comments: Non-reviewed version, original version submitted to CAV 2013; this is a revised version, containing more experimental results and some corrections