arXiv subjects

Alessandro Maria Rizzi

Publications and source records attributed to Alessandro Maria Rizzi.

3 recordsLinked to original sources

arXiv2026

Syntax-driven Incremental Program Verification of Matching Logic Properties

Incrementality is a fundamental design principle to master the complexity of large, long-lived software systems. This principle has been embraced by agile development processes and it lays at the base of continuous software evolution. A major challenge in this context is to incrementally re-verify the correctness of software artifacts after every change, focusing the verification efforts only on the parts affected by the change. We present an approach to the incremental verification of programs written in KernelC, annotated with properties expressed in matching logic. The approach is based on a syntactic-semantic framework that enables analyzing code chunks in isolation so that, after a change to a program fragment, only the part whose semantics is affected by the change is re-processed. This property is obtained by expressing the language syntax through an operator precedence grammar and by formalizing its semantics through a synthesized attribute schema. We have implemented our technique in a prototype tool and experimentally evaluated its effectiveness. The results show that our approach does not penalize the efficiency of formal verification and can outperform program re-verification after changes, depending on the presence and type of annotations, as well as the position of the change and the program structure.

cs.SE↗

arXiv2018

Integrating Topological Proofs with Model Checking to Instrument Iterative Design

System development is not a linear, one-shot process. It proceeds through refinements and revisions. To support assurance that the system satisfies its requirements, it is desirable that continuous verification can be performed after each refinement or revision step. To achieve practical adoption, formal system modeling and verification must accommodate continuous verification efficiently and effectively. Our proposal to address this problem is TOrPEDO, a verification approach where models are given via Partial Kripke Structures (PKSs) and requirements are specified as Linear-time Temporal Logic (LTL) properties. PKSs support refinement, by deliberately indicating unspecified parts of the model that are later completed. We support verification in two complementary forms: via model checking and proofs. Model checking is useful to provide counterexamples, i.e., pinpoint model behaviors that violate requirements. Proofs are instead useful since they can explain why requirements are satisfied. In our work, we introduce a specific concept of proof, called topological proof (TP). A TP produces a slice of the original PKS which justifies the property satisfaction. Because models can be incomplete, TOrPEDO supports reasoning on requirements satisfaction, violation, and possible satisfaction (in the case where the satisfaction depends on unknown parts).

cs.LO↗

arXiv2016

Support vector regression model for BigData systems

Nowadays Big Data are becoming more and more important. Many sectors of our economy are now guided by data-driven decision processes. Big Data and business intelligence applications are facilitated by the MapReduce programming model while, at infrastructural layer, cloud computing provides flexible and cost effective solutions for allocating on demand large clusters. In such systems, capacity allocation, which is the ability to optimally size minimal resources for achieve a certain level of performance, is a key challenge to enhance performance for MapReduce jobs and minimize cloud resource costs. In order to do so, one of the biggest challenge is to build an accurate performance model to estimate job execution time of MapReduce systems. Previous works applied simulation based models for modeling such systems. Although this approach can accurately describe the behavior of Big Data clusters, it is too computationally expensive and does not scale to large system. We try to overcome these issues by applying machine learning techniques. More precisely we focus on Support Vector Regression (SVR) which is intrinsically more robust w.r.t other techniques, like, e.g., neural networks, and less sensitive to outliers in the training set. To better investigate these benefits, we compare SVR to linear regression.

cs.DC↗