Electronic Communications of the EASST (European Association of Software Science and Technology)
Not a member yet
887 research outputs found
Sort by
A Unification Algorithm for GP 2
Get PDFThe graph programming language GP 2 allows to apply sets of ruleschemata (or “attributed” rules) non-deterministically. To analyse conflicts of pro-grams statically, graphs labelled with expressisons are overlayed to construct criticalpairs of rule applications. Each overlay induces a system of equations whose solu-tions represent different conflicts. We present a rule-based unification algorithm forGP expressions that is terminating, sound and complete. For every input equation,the algorithm generates a finite set of substitutions. Soundness means that each ofthese substitutions solves the input equation. Since GP labels are lists constructed byconcatenation, unification modulo associativity and unit law is required. This prob-lem, which is also known as word unification, is infinitary in general but becomesfinitary due to GP’s rule schema syntax and the assumption that rule schemata areleft-linear. Our unification algorithm is complete in that every solution of an inputequation is an instance of some substitution in the generated set
Model-based WCET Analysis with Invariants
Get PDFThe integration of worst case execution time (WCET) analysis in model-based designs allows timing problems to be discovered in the early phases of development, when they are less expensive to correct than in later phases. In this paper, we show how model-based WCET analysis can improve timing calculations compared to program-based WCET analysis. The models are described by hierarchical state machines with concurrency, probabilistic transition, stochastic transitions, costs/rewards attached to states and transitions, and invariants attached to states. In these models, user-specified invariants serve to check the correctness of designs by restricting allowed state configurations. Our contribution is to use invariants additionally to determine transition combinations (paths) that can be eliminated from the WCET analysis, with the help of a decision procedure, thus making the analysis more precise. The assembly code of transitions for a specific target is generated and execution time for that code calculated. From the model, a probabilistic timed automaton (PTA) or Markov decision process (MDP) can be created. On that model, execution times of transitions are calculated as costs
Loop Patterns in C Programs
Get PDFIn this work, we conduct a systematic study of loops in C programs. We describe static analyses capable of efficiently identifying definite iteration in C code. Our experiments show that over one third of loops in our benchmarks take this form. To cover further loops, we systematically weaken our definition of definite iteration and derive a family of loop classes that are heuristics for definite iteration. We then measure the occurrence of these classes on real-world C code and investigate which statements are used to express them. Finally, we empirically show that our classification is meaningful -- (a) it describes the majority of loops in our benchmarks, (b) the classes are good heuristics for termination, and (c) they can be used as software metrics to characterize benchmarks for software verification
Distributed execution of bigraphical reactive systems
Get PDFThe bigraph embedding problem is crucial for many results and tools about bigraphs and bigraphical reactive systems (BRS). Current algorithms for computing bigraphical embeddings arecentralized, i.e. designed to run locally with a complete view of the guest and host bigraphs. In order to deal with large bigraphs, and to parallelize reactions, we present adecentralized algorithm, which distributes both state and computation over several concurrent processes. This allows for distributed, parallel simulations where non-interfering reactions can be carried out concurrently; nevertheless, even in the worst case the complexity of this distributed algorithm is no worse than that of a centralized algorithm
Studying Verification Conditions for Imperative Programs
Get PDFProgram verification tools use verification condition generators to produce logical formulas whose validity implies that the program is correct with respect to its specification. Different tools produce different conditions, and the underlying algorithms have not been properly exposed or explored so far. In this paper we consider a simple imperative programming language, extended with assume and assert statements, to present different ways of generating verification conditions. We study the approaches with experimental results originated by verification conditions generated from the intermediate representation of LLVM
Lenses for Web Data
Get PDFPutting data on the web typically involves implementing two transformations: one to convert the data into HTML, and another to parse modifications out of interactions with clients. Unfortunately, in current systems, these transformations are usually implemented using two separate functions—an approach that replicates functionality across multiple pieces of code, and makes programs difficult to write, reason about, and maintain. This paper presents a different approach: an abstraction based on formlets that makes it easy to bridge the gap between data stored on a server and values embedded in HTML forms. We introduce formlenses, which combine the advantages of formlets with those of lenses to provide compositional, bidirectional form-based views of Web data. We show that formlenses can be viewed as monoidal functors over lenses, analogously to formlets, which are applicative functors. Finally, we investigate the connection between linearity and bidirectional transformations and describe a translation from a linear pattern syntax into formlens combinators
Preface of SQM 2014 Proceedings - 8th International Workshop on Software Quality and Maintainability
No full textThe 8th International Workshop on Software Quality and Maintainability (SQM) was co-located with the CSMR-WCRE 2014 Software Evolution Week in Antwerp, Belgium in February 2014. SQM focuses on the boundaries between theory and practice of software quality. This special issue of ECEASST contains 7 papers that have been selected for inclusion in the postproceedings, after a rigorous peer review process and taking into account the feedback received from the reviewers and from the workshop participants
Proceedings of the XIII Spanish Conference on Programming and Computer Languages (PROLE 2013)
Get PDFPrefac
Symbol Elimination for Automated Generation of Program Properties
Get PDFAutomatic understanding of the intended meaning of computer programs is a very hard problem, requiring intelligence and reasoning. In this talk we describe applications of our symbol elimination methods in automated proram analysis. Symbol elimination uses first-order theorem proving techniques in conjunction with symbolic computation methods, and derives nontrivial program properties, such as loop invariants and loop bounds, in a fully automatic way. Moreover, symbol elimination can be used as an alternative to interpolation for software verification
Toward a Code-Clone Search through the Entire Lifecycle of a Software Product
Get PDFThis paper presents a clone-detection method/tool currently under devel-opment. This tool is useful as a code-clone search through the entire lifecycle ofa software product; The tool searches code examples and analyzes of code clonesin both preventive and postmortem ways[LRHK10]. The approach is based on asequence equivalence on execution paths[Kam13] and extends the equivalence toinclude gaps, thus type-3[BKA + 07] clone detection. Each of the detected clones isa sub-sequence of an execution path of a given program, in other words, a set of codefragments of multiple procedures (methods) which can be executed in a run of theprogram. The approach is relaxed in terms of adaptability to incomplete (not-yet-finished) code, but also makes use of concrete information such as types (includinghierarchy) and dynamic dispatch when such information is available