Verification, Model Checking, and Abstract Interpretation
11th International Conference, VMCAI 2010, Madrid, Spain, January 17-19, 2010. Proceedings
Page
%P
56 Result(s)
within
Manuel Hermenegildo
-
Chapter and Conference Paper
Transforming Big-Step to Small-Step Semantics Using Interpreter Specialisation
Natural semantics (big-step) and structural operational semantics (small-step) each have advantages, so it can be useful to produce both semantic forms for a language. Previous work has shown that big-step sem...
-
Chapter and Conference Paper
A Rule-Based Approach for Designing and Composing Abstract Domains
Abstract interpretation allows constructing sound static analysis tools by safely approximating program semantics. Frameworks for abstract interpretation typically provide an implementation of a specialized it...
-
Chapter and Conference Paper
Cost Analysis of Smart Contracts Via Parametric Resource Analysis
The very nature of smart contracts and blockchain platforms, where program execution and storage are replicated across a large number of nodes, makes resource consumption analysis highly relevant. This has led...
-
Chapter and Conference Paper
Interval-Based Resource Usage Verification: Formalization and Prototype
In an increasing number of applications (e.g., in embedded, real-time, or mobile systems) it is important or even essential to ensure conformance with respect to a specification expressing the use of some reso...
-
Chapter and Conference Paper
Constraint-Based Runtime Prediction of SLA Violations in Service Orchestrations
Service compositions put together loosely-coupled component services to perform more complex, higher level, or cross-organizational tasks in a platform-independent manner. Quality-of-Service (QoS) properties, ...
-
Chapter and Conference Paper
Profiling for Run-Time Checking of Computational Properties and Performance Debugging in Logic Programs
Although several profiling techniques for identifying performance bottlenecks in logic programs have been developed, they are generally not automatic and in most cases they do not provide enough information fo...
-
Reference Work Entry In depth
Logic Languages
-
Article
Automatic Inference of Determinacy and Mutual Exclusion for Logic Programs Using Mode and Type Analyses
We propose an analysis for detecting procedures and goals that are deterministic (i.e., that produce at most one solution at most once), or predicates whose clause tests are mutually exclusive (which implies t...
-
Book and Conference Proceedings
-
Chapter and Conference Paper
Automatic Fragment Identification in Workflows Based on Sharing Analysis
In Service-Oriented Computing (SOC), fragmentation and merging of workflows are motivated by a number of concerns, among which we can cite design issues, performance, and privacy. Fragmentation emphasizes the ...
-
Chapter and Conference Paper
An Initial Proposal for Data-Aware Resource Analysis of Orchestrations with Applications to Predictive Monitoring
Several activities in service oriented computing can benefit from knowing ahead of time future properties of a given service composition. In this paper we focus on how statically inferred computational cost fu...
-
Chapter and Conference Paper
Program Parallelization Using Synchronized Pipelining
While there are well-understood methods for detecting loops whose iterations are independent and parallelizing them, there are comparatively fewer proposals that support parallel execution of a sequence of loo...
-
Chapter and Conference Paper
A Tabling Implementation Based on Variables with Multiple Bindings
Suspension-based tabling systems have to save and restore computation states belonging to OR branches. Stack freezing combined with (forward) trailing is among the better-known implementation approaches for th...
-
Chapter and Conference Paper
Integrating Software Testing and Run-Time Checking in an Assertion Verification Framework
We present a framework that unifies unit testing and run-time verification (as well as static verification and static debugging). A key contribution of our overall approach is that we preserve the use of a uni...
-
Article
Abstraction-Carrying Code: a Model for Mobile Code Safety
Proof-Carrying Code (PCC) is a general approach to mobile code safety in which programs are augmented with a certificate (or proof). The intended benefit is that the program consumer can ...
-
Chapter and Conference Paper
Efficient Context-Sensitive Shape Analysis with Graph Based Heap Models
The performance of heap analysis techniques has a significant impact on their utility in an optimizing compiler. Most shape analysis techniques perform interprocedural dataflow analysis in a context-sensitive ...
-
Chapter and Conference Paper
Identification of Heap–Carried Data Dependence Via Explicit Store Heap Models
Dependence information between program values is extensively used in many program optimization techniques. The ability to identify statements, calls and loop iterations that do not depend on each other enables...
-
Chapter and Conference Paper
Towards Description and Optimization of Abstract Machines in an Extension of Prolog
Competitive abstract machines for Prolog are usually large, intricate, and incorporate sophisticated optimizations. This makes them difficult to code, optimize, and, especially, maintain and extend. This is pa...
-
Chapter and Conference Paper
A Static Heap Analysis for Shape and Connectivity: Unified Memory Analysis: The Base Framework
Modeling the evolution of the state of program memory during program execution is critical to many parallelization techniques. Current memory analysis techniques either provide very accurate information but ru...
-
Chapter and Conference Paper
Using Combined Static Analysis and Profiling for Logic Program Execution Time Estimation
Predicting statically the running time of programs has many applications ranging from task scheduling in parallel execution to proving the ability of a program to meet strict time constraints. A starting point...
