6 citations · 14 across the 11 of their papers we have counts for
12 papers
Agentic Generation and Evolution of Knowledge Models
Man Zhang, Tao Yue, Nazareno M. Aguirre +2
Complex software systems such as autonomous vehicles, robotics increasingly interact with dynamic physical, cyber, and social environments. Reasoning about their behavior, maintain…
Improving Dynamic Specification Inference with LLM-Generated Counterexamples
Agustín Balestra, Agustín Nolasco, Facundo Molina +3
Contract assertions, such as preconditions, postconditions, and invariants, play a crucial role in software development, enabling applications such as program verification, test ge…
Live Objects All The Way Down: Removing the Barriers between Applications and Virtual Machines
Javier E. Pimás, Stefan Marr, Diego Garbervetsky
Object-oriented languages often use virtual machines (VMs) that provide mechanisms such as just-in-time (JIT) compilation and garbage collection (GC). These VM components are typic…
Dynamic Slicing by On-demand Re-execution
Ivan Postolski, Victor Braberman, Diego Garbervetsky +1
In this paper, we propose a novel approach that aims to offer an alternative to the prevalent paradigm to dynamic slicing construction. Dynamic slicing requires dynamic data and co…
Focused Dynamic Slicing for Large Applications using an Abstract Memory-Model
Alexis Soifer, Diego Garbervetsky, Victor Braberman +1
Dynamic slicing techniques compute program dependencies to find all statements that affect the value of a variable at a program point for a specific execution. Despite their many p…
InspectJS: Leveraging Code Similarity and User-Feedback for Effective Taint Specification Inference for JavaScript
Saikat Dutta, Diego Garbervetsky, Shuvendu Lahiri +1
Static analysis has established itself as a weapon of choice for detecting security vulnerabilities. Taint analysis in particular is a very general and powerful technique, where se…
Verification Coverage
Rodrigo Castaño, Victor Braberman, Diego Garbervetsky +1
Software Model Checkers have shown outstanding performance improvements in recent times. Moreover, for specific use cases, formal verification techniques have shown to be highly ef…
Model Checker Execution Reports
Rodrigo Castaño, Victor Braberman, Diego Garbervetsky +1
Software model checking constitutes an undecidable problem and, as such, even an ideal tool will in some cases fail to give a conclusive answer. In practice, software model checker…
The DynAlloy Visualizer
Pablo Bendersky, Juan Pablo Galeotti, Diego Garbervetsky
We present an extension to the DynAlloy tool to navigate DynAlloy counterexamples: the DynAlloy Visualizer. The user interface mimics the functionality of a programming language de…
On Verifying Resource Contracts using Code Contracts
Rodrigo Castaño, Juan Pablo Galeotti, Diego Garbervetsky +2
In this paper we present an approach to check resource consumption contracts using an off-the-shelf static analyzer. We propose a set of annotations to support resource usage speci…
Waterfall: Primitives Generation on the Fly
Guido Chari, Diego Garbervetsky, Camillo Bruni +2
Modern languages are typically supported by managed runtimes (Virtual Machines). Since VMs have to deal with many concepts such as memory management, abstract execution model and s…
Reducing the Number of Annotations in a Verification-oriented Imperative Language
Guido de Caso, Diego Garbervetsky, Daniel Gorín
Automated software verification is a very active field of research which has made enormous progress both in theoretical and practical aspects. Recently, an important amount of rese…