Zobrazeno 1 - 10
of 78
pro vyhledávání: '"Samir Genaim"'
Publikováno v:
The Logic of Software. A Tasting Menu of Formal Methods ISBN: 9783031081651
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::cfd3afefd988e40766dacca7113f26ce
https://doi.org/10.1007/978-3-031-08166-8_2
https://doi.org/10.1007/978-3-031-08166-8_2
Publikováno v:
Computer Aided Verification ISBN: 9783030816872
CAV (2)
CAV (2)
This paper presents a new framework to synthesize lower-bounds on the worst-case cost for non-deterministic integer loops. As in previous approaches, the analysis searches for a metering function that under-approximates the number of loop iterations.
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::efbacaab68632967ae2ad986a184bacf
https://doi.org/10.1007/978-3-030-81688-9_40
https://doi.org/10.1007/978-3-030-81688-9_40
Autor:
Jesús J. Doménech, Samir Genaim
Programs with multiphase control-flow are programs where the execution passes through several (possibly implicit) phases. Proving termination of such programs (or inferring corresponding runtime bounds) is often challenging since it requires reasonin
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::dea550aebad9b75798caa51e9f677bd9
In order to automatically infer the resource consumption of programs, analyzers track how data sizes change along program's execution. Typically, analyzers measure the sizes of data by applying norms which are mappings from data to natural numbers th
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::b98a4cb49aed2eba52d0a29f8a0720a7
http://arxiv.org/abs/1908.02078
http://arxiv.org/abs/1908.02078
Publikováno v:
Static Analysis ISBN: 9783030323035
SAS
SAS
Multiphase ranking functions (M\(\varPhi \)RFs) are used to prove termination of loops in which the computation progresses through a number of phases. They consist of linear functions \(\langle f_1,\ldots ,f_d \rangle \) where \(f_i\) decreases durin
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::25c2f2cbe51619200b818a5e3acca1dc
https://doi.org/10.1007/978-3-030-32304-2_22
https://doi.org/10.1007/978-3-030-32304-2_22
Control-flow refinement refers to program transformations whose purpose is to make implicit control-flow explicit, and is used in the context of program analysis to increase precision. Several techniques have been suggested for different programming
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::1279090ef140e4d4bae84894a948516d
Publikováno v:
Journal of Automated Reasoning. 59:47-85
By following a rely-guarantee style of reasoning, we present novel termination and cost analyses for concurrent programs that, in order to prove termination or infer the cost of a considered loop: (1) infer the termination/cost of each loop as if it
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::c0a16c2cc3265073bad2aee7d60e6cd9
https://doi.org/10.1007/s10817-016-9400-6
https://doi.org/10.1007/s10817-016-9400-6
Publikováno v:
ACM Transactions on Computational Logic. 17:1-39
This article presents a may-happen-in-parallel (MHP) analysis for languages with actor-based concurrency . In this concurrency model, actors are the concurrency units such that, when a method is invoked on an actor a 2 from a task executing on actor
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::cfdf3c44babd87273fb621658b6c2ff0
https://doi.org/10.1145/2824255
https://doi.org/10.1145/2824255
Autor:
Elvira Albert, Richard Bubel, Reiner Hähnle, Guillermo Román-Díez, Samir Genaim, Germán Puebla
Publikováno v:
Software & Systems Modeling. 15:987-1012
Static analysis tools, such as resource analyzers, give useful information on software systems, especially in real-time and safety-critical applications. Therefore, the question of the reliability of the obtained results is highly important. State-of
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::e3c3fcfec6c33d6a800f127b84bd7c7d
https://doi.org/10.1007/s10270-015-0476-y
https://doi.org/10.1007/s10270-015-0476-y
Autor:
Germán Puebla, Jesús Correas, Miguel Gómez-Zamalloa, Samir Genaim, Guillermo Román-Díez, Puri Arenas, Elvira Albert
Publikováno v:
Software Testing, Verification and Reliability. 25:218-271
This article presents a novel cost analysis framework for concurrent objects. Concurrent objects form a well-established model for distributed concurrent systems. In this model, objects are the concurrency units that communicate among them via asynch
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::8a30c1fa84ccc3634be1b6b4be92bad5
https://doi.org/10.1002/stvr.1569
https://doi.org/10.1002/stvr.1569