Showing 1–8 of 8 results for author: Deligiannis, P

Finding Inductive Loop Invariants using Large Language Models

Authors: Adharsh Kamath, Aditya Senthilnathan, Saikat Chakraborty, Pantazis Deligiannis, Shuvendu K. Lahiri, Akash Lal, Aseem Rastogi, Subhajit Roy, Rahul Sharma

Abstract: Loop invariants are fundamental to reasoning about programs with loops. They establish properties about a given loop's behavior. When they additionally are inductive, they become useful for the task of formal verification that seeks to establish strong mathematical guarantees about program's runtime behavior. The inductiveness ensures that the invariants can be checked locally without consulting t… ▽ More Loop invariants are fundamental to reasoning about programs with loops. They establish properties about a given loop's behavior. When they additionally are inductive, they become useful for the task of formal verification that seeks to establish strong mathematical guarantees about program's runtime behavior. The inductiveness ensures that the invariants can be checked locally without consulting the entire program, thus are indispensable artifacts in a formal proof of correctness. Finding inductive loop invariants is an undecidable problem, and despite a long history of research towards practical solutions, it remains far from a solved problem. This paper investigates the capabilities of the Large Language Models (LLMs) in offering a new solution towards this old, yet important problem. To that end, we first curate a dataset of verification problems on programs with loops. Next, we design a prompt for exploiting LLMs, obtaining inductive loop invariants, that are checked for correctness using sound symbolic tools. Finally, we explore the effectiveness of using an efficient combination of a symbolic tool and an LLM on our dataset and compare it against a purely symbolic baseline. Our results demonstrate that LLMs can help improve the state-of-the-art in automated program verification. △ Less

Submitted 14 November, 2023; originally announced November 2023.

Fixing Rust Compilation Errors using LLMs

Authors: Pantazis Deligiannis, Akash Lal, Nikita Mehrotra, Aseem Rastogi

Abstract: The Rust programming language, with its safety guarantees, has established itself as a viable choice for low-level systems programming language over the traditional, unsafe alternatives like C/C++. These guarantees come from a strong ownership-based type system, as well as primitive support for features like closures, pattern matching, etc., that make the code more concise and amenable to reasonin… ▽ More The Rust programming language, with its safety guarantees, has established itself as a viable choice for low-level systems programming language over the traditional, unsafe alternatives like C/C++. These guarantees come from a strong ownership-based type system, as well as primitive support for features like closures, pattern matching, etc., that make the code more concise and amenable to reasoning. These unique Rust features also pose a steep learning curve for programmers. This paper presents a tool called RustAssistant that leverages the emergent capabilities of Large Language Models (LLMs) to automatically suggest fixes for Rust compilation errors. RustAssistant uses a careful combination of prompting techniques as well as iteration with an LLM to deliver high accuracy of fixes. RustAssistant is able to achieve an impressive peak accuracy of roughly 74% on real-world compilation errors in popular open-source Rust repositories. We plan to release our dataset of Rust compilation errors to enable further research. △ Less

Submitted 9 August, 2023; originally announced August 2023.

Efficient Parabolic Optimisation Algorithm for adaptive VQE implementations

Authors: V. Armaos, Dimitrios A. Badounas, Paraskevas Deligiannis, Konstantinos Lianos, Yordan S. Yordanov

Abstract: Computational chemistry is one of the most promising applications of quantum computing, mostly thanks to the development of the Variational Quantum Eigensolver (VQE) algorithm. VQE is being studied extensively and numerous optimisations of VQE's sub-processes have been suggested, including the encoding methods and the choice of excitations. Recently, adaptive methods were introduced that apply eac… ▽ More Computational chemistry is one of the most promising applications of quantum computing, mostly thanks to the development of the Variational Quantum Eigensolver (VQE) algorithm. VQE is being studied extensively and numerous optimisations of VQE's sub-processes have been suggested, including the encoding methods and the choice of excitations. Recently, adaptive methods were introduced that apply each excitation iteratively. When it comes to adaptive VQE, research is focused on the choice of excitation pool and the strategies for choosing each excitation. Here we focus on a usually overlooked component of VQE, which is the choice of the classical optimisation algorithm. We introduce the parabolic optimiser that we designed specifically for the needs of VQE. This includes both an 1-D and an n-D optimiser that can be used either for adaptive or traditional VQE implementations. We then continue to benchmark the parabolic optimiser against Nelder-Mead for various implementations of VQE. We found that the parabolic optimiser performs significantly better than traditional optimisation methods, requiring fewer CNOTs and fewer quantum experiments to achieve a given energy accuracy. △ Less

Submitted 25 October, 2021; originally announced October 2021.

Studying Ransomware Attacks Using Web Search Logs

Authors: Chetan Bansal, Pantazis Deligiannis, Chandra Maddila, Nikitha Rao

Abstract: Cyber attacks are increasingly becoming prevalent and causing significant damage to individuals, businesses and even countries. In particular, ransomware attacks have grown significantly over the last decade. We do the first study on mining insights about ransomware attacks by analyzing query logs from Bing web search engine. We first extract ransomware related queries and then build a machine lea… ▽ More Cyber attacks are increasingly becoming prevalent and causing significant damage to individuals, businesses and even countries. In particular, ransomware attacks have grown significantly over the last decade. We do the first study on mining insights about ransomware attacks by analyzing query logs from Bing web search engine. We first extract ransomware related queries and then build a machine learning model to identify queries where users are seeking support for ransomware attacks. We show that user search behavior and characteristics are correlated with ransomware attacks. We also analyse trends in the temporal and geographical space and validate our findings against publicly available information. Lastly, we do a case study on 'Nemty', a popular ransomware, to show that it is possible to derive accurate insights about cyber attacks by query log analysis. △ Less

Submitted 23 May, 2020; v1 submitted 1 May, 2020; originally announced May 2020.

Comments: To appear in the proceedings of SIGIR 2020

Building Reliable Cloud Services Using P# (Experience Report)

Authors: Pantazis Deligiannis, Narayanan Ganapathy, Akash Lal, Shaz Qadeer

Abstract: Cloud services must typically be distributed across a large number of machines in order to make use of multiple compute and storage resources. This opens the programmer to several sources of complexity such as concurrency, order of message delivery, lossy network, timeouts and failures, all of which impose a high cognitive burden. This paper presents evidence that technology inspired by formal-met… ▽ More Cloud services must typically be distributed across a large number of machines in order to make use of multiple compute and storage resources. This opens the programmer to several sources of complexity such as concurrency, order of message delivery, lossy network, timeouts and failures, all of which impose a high cognitive burden. This paper presents evidence that technology inspired by formal-methods, delivered as part of a programming framework, can help address these challenges. In particular, we describe the experience of several engineering teams in Microsoft Azure that used the open-source P# programming framework to build multiple reliable cloud services. P# imposes a principled design pattern that allows writing formal specifications alongside production code that can be systematically tested, without deviating from routine engineering practices. Engineering teams that have been using P# have reported dramatically increased productivity (in time taken to push new features to production) as well as services that have been running live for months without any issues in features developed and tested with P#. △ Less

Submitted 12 February, 2020; originally announced February 2020.

Computational Chemistry on Quantum Computers: Ground state estimation

Authors: V. Armaos, Dimitrios A. Badounas, Paraskevas Deligiannis

Abstract: We present computational chemistry data for small molecules ($CO$, $HCl$, $F_2$, $NH_4^+$, $CH_4$, $NH_{3}$, $H_3O^+$, $H{_2}O$, $BeH_{2}$, $LiH$, $OH^-$, $HF$, $HeH^+$, $H_2$), obtained by implementing the Unitary Coupled Cluster method with Single and Double excitations (UCCSD) on a quantum computer simulator. We have used the Variational Quantum Eigensolver (VQE) algorithm to extract the ground… ▽ More We present computational chemistry data for small molecules ($CO$, $HCl$, $F_2$, $NH_4^+$, $CH_4$, $NH_{3}$, $H_3O^+$, $H{_2}O$, $BeH_{2}$, $LiH$, $OH^-$, $HF$, $HeH^+$, $H_2$), obtained by implementing the Unitary Coupled Cluster method with Single and Double excitations (UCCSD) on a quantum computer simulator. We have used the Variational Quantum Eigensolver (VQE) algorithm to extract the ground state energies of these molecules. This energy data represents the expected ground state energy that a quantum computer will produce for the given molecules, on the STO-3G basis. Since there is a lot of interest in the implementation of UCCSD on quantum computers, we hope that our work will serve as a benchmark for future experimental implementations. △ Less

Submitted 30 June, 2019; originally announced July 2019.

Reliable State Machines: A Framework for Programming Reliable Cloud Services

Authors: Suvam Mukherjee, Nitin John Raj, Krishnan Govindraj, Pantazis Deligiannis, Chandramouleswaran Ravichandran, Akash Lal, Aseem Rastogi, Raja Krishnaswamy

Abstract: Building reliable applications for the cloud is challenging because of unpredictable failures during a program's execution. This paper presents a programming framework called Reliable State Machines (RSMs), that offers fault-tolerance by construction. Using our framework, a programmer can build an application as several (possibly distributed) RSMs that communicate with each other via messages, muc… ▽ More Building reliable applications for the cloud is challenging because of unpredictable failures during a program's execution. This paper presents a programming framework called Reliable State Machines (RSMs), that offers fault-tolerance by construction. Using our framework, a programmer can build an application as several (possibly distributed) RSMs that communicate with each other via messages, much in the style of actor-based programming. Each RSM is additionally fault-tolerant by design and offers the illusion of being "always-alive". An RSM is guaranteed to process each input request exactly once, as one would expect in a failure-free environment. The RSM runtime automatically takes care of persisting state and rehydrating it on a failover. We present the core syntax and semantics of RSMs, along with a formal proof of failure-transparency. We provide an implementation of the RSM framework and runtime on the .NET platform for deploying services to Microsoft Azure. We carried out an extensive performance evaluation on micro-benchmarks to show that one can build high-throughput applications with RSMs. We also present a case study where we rewrote a significant part of a production cloud service using RSMs. The resulting service has simpler code and exhibits production-grade performance. △ Less

Submitted 27 February, 2019; v1 submitted 25 February, 2019; originally announced February 2019.

Comments: R1: This replacement contains minor formatting improvements over the original R2: Anonymized "popular cloud service provider" phrase replaced with "Microsoft Azure"

Implementing and Evaluating Candidate-Based Invariant Generation

Authors: Adam Betts, Nathan Chong, Pantazis Deligiannis, Alastair F. Donaldson, Jeroen Ketema

Abstract: The discovery of inductive invariants lies at the heart of static program verification. Presently, many automatic solutions to inductive invariant generation are inflexible, only applicable to certain classes of programs, or unpredictable. An automatic technique that circumvents these deficiencies to some extent is candidate-based invariant generation. This paper describes our efforts to apply can… ▽ More The discovery of inductive invariants lies at the heart of static program verification. Presently, many automatic solutions to inductive invariant generation are inflexible, only applicable to certain classes of programs, or unpredictable. An automatic technique that circumvents these deficiencies to some extent is candidate-based invariant generation. This paper describes our efforts to apply candidate-based invariant generation in GPUVerify, a static checker for programs that run on GPUs. We study a set of GPU programs that contain loops, drawn from a number of open source suites and vendor SDKs. We describe the methodology we used to incrementally improve the invariant generation capabilities of GPUVerify to handle these benchmarks, through candidate-based invariant generation, using cheap static analysis to speculate potential program invariants. We also describe a set of experiments that we used to examine the effectiveness of our rules for candidate generation, assessing rules based on their generality (the extent to which they generate candidate invariants), hit rate (the extent to which the generated candidates hold), worth (the extent to which provable candidates actually help in allowing verification to succeed), and influence (the extent to which the success of one generation rule depends on candidates generated by another rule). The candidates produced by GPUVerify help to verify 231 of the 253 programs. This increase in precision, however, makes GPUVerify sluggish: the more candidates that are generated, the more time is spent determining which are inductive invariants. To speed up this process, we have investigated four under-approximating program analyses that aim to reject false candidates quickly and a framework whereby these analyses can run in sequence or in parallel. △ Less

Submitted 15 June, 2017; v1 submitted 4 December, 2016; originally announced December 2016.