International Journal on Software Tools for Technology Transfer
Công bố khoa học tiêu biểu
* Dữ liệu chỉ mang tính chất tham khảo
Sắp xếp:
Verifying a quantitative relaxation of linearizability via refinement
International Journal on Software Tools for Technology Transfer - Tập 18 - Trang 393-407 - 2015
The recent years have seen increasingly widespread use of highly concurrent data structures in both multi-core and distributed computing environments, thereby escalating the priority for verifying their correctness. Quasi linearizability is a quantitative variation of the standard linearizability correctness condition to allow more implementation freedom for performance optimization. However, ensu...... hiện toàn bộ
Algorithmic program synthesis: introduction
International Journal on Software Tools for Technology Transfer - Tập 15 - Trang 397-411 - 2013
Program synthesis is a process of producing an executable program from a specification. Algorithmic synthesis produces the program automatically, without an intervention from an expert. While classical compilation falls under the definition of algorithmic program synthesis, with the source program being the specification, the synthesis literature is typically concerned with producing programs that...... hiện toàn bộ
Program slicing for VHDL
International Journal on Software Tools for Technology Transfer - Tập 4 - Trang 125-137 - 2002
Hardware description languages (HDLs) are used today to describe circuits at all levels. In large HDL programs, there is a need for source code reduction techniques to address a myriad of problems in design, simulation, testing, and formal verification. Program slicing is a static program analysis technique that allows an analyst to automatically extract portions of programs relevant to the aspect...... hiện toàn bộ
Model-checking multi-threaded distributed Java programs
International Journal on Software Tools for Technology Transfer - Tập 4 - Trang 71-91 - 2002
State-space exploration is a powerful technique for verification of concurrent software systems. Applying it to software systems written in standard programming languages requires powerful abstractions (of data) and reductions (of atomicity), which focus on simplifying the data and control, respectively, by aggregation. We propose a reduction that exploits a common pattern of synchronization, name...... hiện toàn bộ
Fast detection of concurrency errors by state space traversal with randomization and early backtracking
International Journal on Software Tools for Technology Transfer - Tập 21 Số 4 - Trang 365-400 - 2019
Distributed reachability analysis in timed automata
International Journal on Software Tools for Technology Transfer - Tập 7 - Trang 19-30 - 2003
We evaluate a distributed reachability algorithm suitable for verification of real time critical systems modeled as timed automata. It is discovered that the algorithm suffers from load balancing problems and a high communication overhead. The load balancing problems are caused by the symbolic nature of the representation of the states of a timed automaton. We propose alternative data structures f...... hiện toàn bộ
CADP 2011: a toolbox for the construction and analysis of distributed processes
International Journal on Software Tools for Technology Transfer - Tập 15 - Trang 89-107 - 2012
CADP (Construction and Analysis of Distributed Processes) is a comprehensive software toolbox that implements the results of concurrency theory. Started in the mid-1980s, CADP has been continuously developed by adding new tools and enhancing existing ones. Today, CADP benefits from a worldwide user community, both in academia and industry. This paper presents the latest release, CADP 2011, which i...... hiện toàn bộ
A loop acceleration technique to speed up verification of automatically generated plans
International Journal on Software Tools for Technology Transfer - Tập 16 - Trang 13-29 - 2013
The CIRCA planning system automatically creates reactive plans and uses formal verification techniques to prove that those plans will preserve system safety. CIRCA’s timed automata verification system is highly efficient, yet can display pathologically bad behavior when reasoning about reaction loops, a particular form of interacting cycles of states. In this paper, we describe a loop acceleration...... hiện toàn bộ
Introduction to the Special Issue devoted to SPIN 2018
International Journal on Software Tools for Technology Transfer - Tập 22 - Trang 103-104 - 2020
Healing Web applications through automatic workarounds
International Journal on Software Tools for Technology Transfer - Tập 10 - Trang 493-502 - 2008
We develop the notion of automatic workaround in the context of Web applications. A workaround is a sequence of operations, applied to a failing component, that is equivalent to the failing sequence in terms of its intended effect, but that does not result in a failure. We argue that workarounds exist in modular systems because components often offer redundant interfaces and implementations, which...... hiện toàn bộ
Tổng số: 667
- 1
- 2
- 3
- 4
- 5
- 6
- 10