13 citations · 42 across the 13 of their papers we have counts for
18 papers
Inductive Predicate Synthesis Modulo Programs (Extended)
Scott Wesley, Maria Christakis, Jorge A. Navas +3
A growing trend in program analysis is to encode verification conditions within the language of the input program. This simplifies the design of analysis tools by utilizing off-the…
Towards Translating Real-World Code with LLMs: A Study of Translating to Rust
Hasan Ferit Eniser, Hanliang Zhang, Cristina David +5
Large language models (LLMs) show promise in code translation - the task of translating code written in one programming language to another language - due to their ability to write…
Automatically Testing Functional Properties of Code Translation Models
Hasan Ferit Eniser, Valentin Wüstholz, Maria Christakis
Large language models are becoming increasingly practical for translating code across programming languages, a process known as . Even though automated transpilation s…
Synthesizing a Progression of Subtasks for Block-Based Visual Programming Tasks
Alperen Tercan, Ahana Ghosh, Hasan Ferit Eniser +2
Block-based visual programming environments play an increasingly important role in introducing computing concepts to K-12 students. In recent years, they have also gained popularit…
Specifying and Testing -Safety Properties for Machine-Learning Models
Maria Christakis, Hasan Ferit Eniser, Jörg Hoffmann +2
Machine-learning models are becoming increasingly prevalent in our lives, for instance assisting in image-classification or decision-making tasks. Consequently, the reliability of…
Compositional Verification of Smart Contracts Through Communication Abstraction (Extended)
Scott Wesley, Maria Christakis, Jorge A. Navas +3
Solidity smart contracts are programs that manage up to 2^160 users on a blockchain. Verifying a smart contract relative to all users is intractable due to state explosion. Existin…
Automatically Tailoring Static Analysis to Custom Usage Scenarios
Muhammad Numair Mansur, Benjamin Mariano, Maria Christakis +2
In recent years, there has been significant progress in the development and industrial adoption of static analyzers. Such analyzers typically provide a large, if not huge, number o…
Synthesizing Tasks for Block-based Programming
Umair Z. Ahmed, Maria Christakis, Aleksandr Efremov +4
Block-based visual programming environments play a critical role in introducing computing concepts to K-12 students. One of the key pedagogical challenges in these environments is…
Detecting Critical Bugs in SMT Solvers Using Blackbox Mutational Fuzzing
Muhammad Numair Mansur, Maria Christakis, Valentin Wüstholz +1
Formal methods use SMT solvers extensively for deciding formula satisfiability, for instance, in software verification, systematic test generation, and program synthesis. However,…
RAID: Randomized Adversarial-Input Detection for Neural Networks
Hasan Ferit Eniser, Maria Christakis, Valentin Wüstholz
In recent years, neural networks have become the default choice for image classification and many other learning tasks, even though they are vulnerable to so-called adversarial att…
Perfectly Parallel Fairness Certification of Neural Networks
Caterina Urban, Maria Christakis, Valentin Wüstholz +1
Recently, there is growing concern that machine-learning models, which currently assist or even automate decision making, reproduce, and in the worst case reinforce, bias of the tr…
DeepSearch: A Simple and Effective Blackbox Attack for Deep Neural Networks
Fuyuan Zhang, Sankalan Pal Chowdhury, Maria Christakis
Although deep neural networks have been very successful in image-classification tasks, they are prone to adversarial attacks. To generate adversarial inputs, there has emerged a wi…
Targeted Greybox Fuzzing with Static Lookahead Analysis
Valentin Wüstholz, Maria Christakis
Automatic test generation typically aims to generate inputs that explore new paths in the program under test in order to find bugs. Existing work has, therefore, focused on guiding…
Harvey: A Greybox Fuzzer for Smart Contracts
Valentin Wüstholz, Maria Christakis
We present Harvey, an industrial greybox fuzzer for smart contracts, which are programs managing accounts on a blockchain. Greybox fuzzing is a lightweight test-generation approach…
Differentially Testing Soundness and Precision of Program Analyzers
Christian Klinger, Maria Christakis, Valentin Wüstholz
In the last decades, numerous program analyzers have been developed both by academia and industry. Despite their abundance however, there is currently no systematic way of comparin…
Learning Inputs in Greybox Fuzzing
Valentin Wüstholz, Maria Christakis
Greybox fuzzing is a lightweight testing approach that effectively detects bugs and security vulnerabilities. However, greybox fuzzers randomly mutate program inputs to exercise ne…
Specification Mining for Smart Contracts with Automatic Abstraction Tuning
Florentin Guth, Valentin Wüstholz, Maria Christakis +1
Smart contracts are programs that manage digital assets according to a certain protocol, expressing for instance the rules of an auction. Understanding the possible behaviors of a…
Failure-Directed Program Trimming (Extended Version)
Kostas Ferles, Valentin Wüstholz, Maria Christakis +1
This paper describes a new program simplification technique called program trimming that aims to improve the scalability and precision of safety checking tools. Given a program ${\…