References of "Science of Computer Programming"
     in
Bookmark and Share    
Full Text
Peer Reviewed
See detailA new decomposition-based method for detecting attractors in synchronous Boolean networks
Yuan, Qixia; Mizera, Andrzej UL; Pang, Jun UL et al

in Science of Computer Programming (2019), 180

Detailed reference viewed: 24 (1 UL)
Full Text
Peer Reviewed
See detailUniversal (Meta-)Logical Reasoning: Recent Successes
Benzmüller, Christoph UL

in Science of Computer Programming (2018)

Classical higher-order logic, when utilized as a meta-logic in which various other (classical and non-classical) logics can be shallowly embedded, is suitable as a foundation for the development of a ... [more ▼]

Classical higher-order logic, when utilized as a meta-logic in which various other (classical and non-classical) logics can be shallowly embedded, is suitable as a foundation for the development of a universal logical reasoning engine. Such an engine may be employed, as already envisioned by Leibniz, to support the rigorous formalisation and deep logical analysis of rational arguments on the computer. A respective universal logical reasoning framework is described in this article and a range of successful first applications in philosophy, artificial intelligence and mathematics are surveyed. [less ▲]

Detailed reference viewed: 64 (1 UL)
Full Text
Peer Reviewed
See detailTowards the Systematic Analysis of Non-Functional Properties in Model-Based Engineering for Real-Time Embedded Systems
Brau, Guillaume UL; Navet, Nicolas UL; Hugues, Jérôme

in Science of Computer Programming (2018), 156

The real-time scheduling theory provides analytical methods to assess the temporal predictability of embedded systems. Nevertheless, their use is limited in a Model-Based Systems Engineering approach. In ... [more ▼]

The real-time scheduling theory provides analytical methods to assess the temporal predictability of embedded systems. Nevertheless, their use is limited in a Model-Based Systems Engineering approach. In fact, the large number of applicability conditions makes the use of real-time scheduling analysis tedious and error-prone. Key issues are left to the engineers: when to apply a real-time scheduling analysis? What to do with the analysis results?} This article presents an approach to systematize and then automate the analysis of non-functional properties in Model-Based Systems Engineering. First, preconditions and postconditions define the applicability of an analysis. In addition, contracts specify the analysis interfaces, thereby enabling to reason about the analysis process. We present a proof-of-concept implementation of our approach using a combination of constraint languages (REAL for run-time analysis) and specification languages (Alloy for describing interfaces and reasoning about them). This approach is experimented on architectural models written with the Architecture Analysis and Design Language (AADL). [less ▲]

Detailed reference viewed: 110 (9 UL)
Full Text
Peer Reviewed
See detailAgile Validation of Model Transformations using Compound F-Alloy Specifications
Gammaitoni, Loïc UL; Kelsen, Pierre UL; Ma, Qin

in Science of Computer Programming (2017)

Model transformations play a key role in model driven software engineering approaches. Validation of model transformations is crucial for the quality assurance of software systems to be constructed. The ... [more ▼]

Model transformations play a key role in model driven software engineering approaches. Validation of model transformations is crucial for the quality assurance of software systems to be constructed. The relational logic based specification language Alloy and its accompanying tool the Alloy Analyzer have been used in the past to validate properties of model transformations. However Alloy based analysis of transformations suffers from several limitations. On one hand, it is time consuming and does not scale well. On the other hand, the reliance on Alloy, being a formal method, prevents the effective involvement of domain experts in the validation process which is crucial for pinpointing domain pertinent errors. Those limitations are even more severe when it comes to transformations whose input and/or output are themselves transformations (called compound transformations) because they are inherently more complex. To tackle the performance and scalability limitations, in previous work, we proposed an Alloy-based Domain Specific Language (DSL), called F-Alloy, that is tailored for model transformation specifications. Instead of pure analysis based validation, F-Alloy speeds up the validation of model transformations by applying a hybrid strategy that combines analysis with interpretation. In this paper, we formalize the notion of “hybrid analysis” and further extended it to also support efficient validation of compound transformations. To enable the effective involvement of domain experts in the validation process, we propose in this paper a new approach to model transformation validation, called Visualization-Based Validation (briefly VBV). Following VBV, representative instances of a to-be-validated model transformation are automatically generated by hybrid analysis and shown to domain experts for feedback in a visual notation that they are familiar with. We prescribe a process to guide the application of VBV to model transformations and illustrate it with a benchmark model transformation. [less ▲]

Detailed reference viewed: 103 (4 UL)
Full Text
Peer Reviewed
See detailEventML: Specification, Verification, and Implementation of Crash-Tolerant State Machine Replication Systems
Rahli, Vincent UL; Guaspari, David; Bickford, Mark et al

in Science of Computer Programming (2017)

Detailed reference viewed: 68 (4 UL)
See detailSelected and extended papers from ACM SVT 2014
Pang, Jun UL; Stoelinga, Marielle

in Science of Computer Programming (2016)

Detailed reference viewed: 69 (4 UL)
Full Text
Peer Reviewed
See detailSyntactic-Semantic Incrementality for Agile Verification
Bianculli, Domenico UL; Filieri, Antonio; Ghezzi, Carlo et al

in Science of Computer Programming (2015), 97(0), 47-54

Modern software systems are continuously evolving, often because systems requirements change over time. Responding to requirements changes is one of the principles of agile methodologies. In this paper we ... [more ▼]

Modern software systems are continuously evolving, often because systems requirements change over time. Responding to requirements changes is one of the principles of agile methodologies. In this paper we envision the seamless integration of automated verification techniques within agile methodologies, thanks to the support for incrementality. Incremental verification accommodates the changes that occur within the schedule of frequent releases of software agile processes. We propose a general approach to developing families of verifiers that can support incremental verification for different kinds of artifacts and properties. The proposed syntactic-semantic approach is rooted in operator precedence grammars and their support for incremental parsing. Incremental verification procedures are encoded as attribute grammars, whose incremental evaluation goes hand in hand with incremental parsing. [less ▲]

Detailed reference viewed: 187 (33 UL)
Full Text
Peer Reviewed
See detailMitigating the Effects of Equivalent Mutants with Mutant Classification Strategies
Papadakis, Mike UL; Delamaro, Eduardo Márcio; Le Traon, Yves UL

in Science of Computer Programming (2014), 95

Mutation Testing has been shown to be a powerful technique in detecting software faults. Despite this advantage, in practice there is a need to deal with the equivalent mutants’ problem. Automatically ... [more ▼]

Mutation Testing has been shown to be a powerful technique in detecting software faults. Despite this advantage, in practice there is a need to deal with the equivalent mutants’ problem. Automatically detecting equivalent mutants is an undecidable problem. Therefore, identifying equivalent mutants is cumbersome since it requires manual analysis, resulting in unbearable testing cost. To overcome this difficulty, researchers suggested the use of mutant classification, an approach that aims at isolating equivalent mutants automatically. From this perspective, the present paper establishes and empirically assesses possible mutant classification strategies. A conducted study reveals that mutant classification isolates equivalent mutants effectively when low quality test suites are used. However, it turns out that as the test suites evolve, the benefit of this practice is reduced. Thus, mutant classification is only fruitful in improving test suites of low quality and only up to a certain limit. To this end, empirical results show that the proposed strategies provide a cost-effective solution when they consider a small number of live mutants, i.e., 10-12. At this point they kill 92% of all the killable mutants. [less ▲]

Detailed reference viewed: 118 (10 UL)
Full Text
Peer Reviewed
See detailA verified algebra for read-write Linked Data
Horne, Ross James UL; Sassone, Vladimiro

in Science of Computer Programming (2014), 89

Detailed reference viewed: 40 (1 UL)
Full Text
See detailSpecial issue on software verification and testing (editorial message)
Mousavi, MohammadReza; Pang, Jun UL

in Science of Computer Programming (2014), 95(3), 273-274

Detailed reference viewed: 36 (0 UL)
Peer Reviewed
See detailSpecial issue on Security and Trust
Mauw, Sjouke UL; Massacci, F.; Piessens, F.

in Science of Computer Programming (2008), 74(1-2), 164

Detailed reference viewed: 31 (1 UL)