kth.sePublications
Change search
Link to record
Permanent link

Direct link
Publications (10 of 64) Show all publications
Amilon, J., Esen, Z., Gurov, D., Lidström, C. & Rümmer, P. (2024). An Exercise in Mind Reading: Automatic Contract Inference for Frama-C. In: Guide to Software Verification with Frama-C: Core Components, Usages, and Applications: . Springer Nature
Open this publication in new window or tab >>An Exercise in Mind Reading: Automatic Contract Inference for Frama-C
Show others...
2024 (English)In: Guide to Software Verification with Frama-C: Core Components, Usages, and Applications, Springer Nature, 2024Chapter in book (Other academic)
Place, publisher, year, edition, pages
Springer Nature, 2024
National Category
Computer Sciences
Identifiers
urn:nbn:se:kth:diva-343806 (URN)
Note

QC 20240226

Available from: 2024-02-23 Created: 2024-02-23 Last updated: 2024-02-26Bibliographically approved
Amilon, J., Esen, Z., Gurov, D., Lidström, C. & Rümmer, P. (2023). Automatic Program Instrumentation for Automatic Verification. In: Computer Aided Verification: 35th International Conference, CAV 2023, Proceedings. Paper presented at 35th International Conference on Computer Aided Verification, CAV 2023, Paris, France, Jul 17 2023 - Jul 22 2023 (pp. 281-304). Springer Nature
Open this publication in new window or tab >>Automatic Program Instrumentation for Automatic Verification
Show others...
2023 (English)In: Computer Aided Verification: 35th International Conference, CAV 2023, Proceedings, Springer Nature , 2023, p. 281-304Conference paper, Published paper (Refereed)
Abstract [en]

In deductive verification and software model checking, dealing with certain specification language constructs can be problematic when the back-end solver is not sufficiently powerful or lacks the required theories. One way to deal with this is to transform, for verification purposes, the program to an equivalent one not using the problematic constructs, and to reason about its correctness instead. In this paper, we propose instrumentation as a unifying verification paradigm that subsumes various existing ad-hoc approaches, has a clear formal correctness criterion, can be applied automatically, and can transfer back witnesses and counterexamples. We illustrate our approach on the automated verification of programs that involve quantification and aggregation operations over arrays, such as the maximum value or sum of the elements in a given segment of the array, which are known to be difficult to reason about automatically. We implement our approach in the MonoCera tool, which is tailored to the verification of programs with aggregation, and evaluate it on example programs, including SV-COMP programs.

Place, publisher, year, edition, pages
Springer Nature, 2023
National Category
Computer Sciences
Identifiers
urn:nbn:se:kth:diva-336732 (URN)10.1007/978-3-031-37709-9_14 (DOI)2-s2.0-85169431034 (Scopus ID)
Conference
35th International Conference on Computer Aided Verification, CAV 2023, Paris, France, Jul 17 2023 - Jul 22 2023
Note

Part of ISBN 9783031377082

QC 20231123

Available from: 2023-09-19 Created: 2023-09-19 Last updated: 2024-02-23Bibliographically approved
Lidström, C. & Gurov, D. (2023). Contract Based Embedded Software Design. In: Theoretical Aspects of Software Engineering - 17th International Symposium, TASE 2023, Proceedings: . Paper presented at 17th International Symposium on Theoretical Aspects of Software Engineering, TASE 2023, Bristol, United Kingdom of Great Britain and Northern Ireland, Jul 4 2023 - Jul 6 2023 (pp. 77-94). Springer Nature
Open this publication in new window or tab >>Contract Based Embedded Software Design
2023 (English)In: Theoretical Aspects of Software Engineering - 17th International Symposium, TASE 2023, Proceedings, Springer Nature , 2023, p. 77-94Conference paper, Published paper (Refereed)
Abstract [en]

In embedded systems development, contract based design is a design paradigm where a system is divided hierarchically into components and developed in a top-down manner, using contracts as a means to divide responsibilities and manage the complexity of the system. Contract theories provide a formal basis for reasoning about the properties of the system, and of the contracts themselves. In previous work, we have developed a contract theory for sequential, procedural programs, that is defined abstractly, at the semantic level. The theory fulfils well-established, desired properties of system design. In this paper, we present a methodology for applying the contract theory in real embedded software design. We show how to instantiate the contract theory with concrete syntaxes for defining components and contracts, and how the contract theory enables formal reasoning about the resulting objects. In order to cope with the need for different behavioural models at different levels of abstraction in an embedded system, we extend the contract theory through parametrisation on the semantic domain. We illustrate the application of the proposed methodology on a small, but realistic example, where the temporal logic TLA is used for reasoning at the system level, while lower level components are specified using pre- and post-conditions in the form of ACSL, a specification language for C.

Place, publisher, year, edition, pages
Springer Nature, 2023
National Category
Computer Sciences Embedded Systems
Identifiers
urn:nbn:se:kth:diva-334440 (URN)10.1007/978-3-031-35257-7_5 (DOI)2-s2.0-85164908794 (Scopus ID)
Conference
17th International Symposium on Theoretical Aspects of Software Engineering, TASE 2023, Bristol, United Kingdom of Great Britain and Northern Ireland, Jul 4 2023 - Jul 6 2023
Note

Part of ISBN 9783031352560

QC 20230821

Available from: 2023-08-21 Created: 2023-08-21 Last updated: 2024-02-23Bibliographically approved
Bubel, R., Gurov, D., Hahnle, R. & Scaletta, M. (2023). Trace-based Deductive Verification. In: Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning: . Paper presented at 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR 2023, Manizales, Colombia, Jun 4 2023 - Jun 9 2023 (pp. 73-95). EasyChair, 94
Open this publication in new window or tab >>Trace-based Deductive Verification
2023 (English)In: Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, EasyChair , 2023, Vol. 94, p. 73-95Conference paper, Published paper (Refereed)
Abstract [en]

Contracts specifying a procedure’s behavior in terms of pre- and postconditions are essential for scalable software verification, but cannot express any constraints on the events occurring during execution of the procedure. This necessitates to annotate code with intermediate assertions, preventing full specification abstraction. We propose a logic over symbolic traces able to specify recursive procedures in a modular manner that refers to specified programs only in terms of events. We also provide a deduction system based on symbolic execution and induction that we prove to be sound relative to a trace semantics. Our work generalizes contract-based to trace-based deductive verification by extending the notion of state-based contracts to trace-based contracts.

Place, publisher, year, edition, pages
EasyChair, 2023
Keywords
contract-based reasoning, deductive verification, mu-calculus, symbolic execution, trace contracts
National Category
Computer Sciences
Identifiers
urn:nbn:se:kth:diva-335068 (URN)10.29007/vdfd (DOI)2-s2.0-85166468981 (Scopus ID)
Conference
24th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR 2023, Manizales, Colombia, Jun 4 2023 - Jun 9 2023
Note

QC 20230831

Available from: 2023-08-31 Created: 2023-08-31 Last updated: 2023-08-31Bibliographically approved
Gurov, D., Lidström, C. & Rümmer, P. (2022). Alice in Wineland: A Fairy Tale with Contracts. In: The Logic of Software. A Tasting Menu of Formal Methods: (pp. 229-242). Springer Nature
Open this publication in new window or tab >>Alice in Wineland: A Fairy Tale with Contracts
2022 (English)In: The Logic of Software. A Tasting Menu of Formal Methods, Springer Nature , 2022, p. 229-242Chapter in book (Refereed)
Abstract [en]

In this tale Alice ends up in Wineland, where she tries to attend the birthday party of one of its most beloved inhabitants. In order to do so, she must learn about contracts and how important they are. She gets exposed to several contract languages, with their syntax and semantics, such as pre- and post-conditions, state machines, context-free grammars, and interval logic. She learns for what type of properties they are appropriate to use, and how to formally verify that programs meet their contracts.

Place, publisher, year, edition, pages
Springer Nature, 2022
Series
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), ISSN 0302-9743 ; 13360
National Category
Computer Sciences
Identifiers
urn:nbn:se:kth:diva-318003 (URN)10.1007/978-3-031-08166-8_11 (DOI)2-s2.0-85133656076 (Scopus ID)
Note

QC 20220915

Chapter in book: 978-3-031-08165-1

Available from: 2022-09-15 Created: 2022-09-15 Last updated: 2022-09-15Bibliographically approved
Filipovikj, P., Ung, G., Gurov, D. & Nyberg, M. (2022). Bounded Invariant Checking for Stateflow. In: Electronic Proceedings in Theoretical Computer Science, EPTCS: . Paper presented at 4th International Workshop on Formal Methods for Autonomous Systems, FMAS 2022 and 4th International Workshop on Automated and Verifiable Software sYstem DEvelopment, ASYDE 2022, 26-27 September 2022 (pp. 38-52). Open Publishing Association
Open this publication in new window or tab >>Bounded Invariant Checking for Stateflow
2022 (English)In: Electronic Proceedings in Theoretical Computer Science, EPTCS, Open Publishing Association , 2022, p. 38-52Conference paper, Published paper (Refereed)
Abstract [en]

Stateflow models are complex software models, often used as part of industrial safety-critical software solutions designed with Matlab Simulink. Being part of safety-critical solutions, these models require the application of rigorous verification techniques for assuring their correctness. In this paper, we propose a refutation-based formal verification approach for analyzing Stateflow models against invariant properties, based on bounded model checking (BMC). The crux of our technique is: i) a representation of the state space of Stateflow models as a symbolic transition system (STS) over the symbolic configurations of the model, and ii) application of incremental BMC, to generate verification results after each unrolling of the next-state relation of the transition system. To this end, we develop a symbolic structural operational semantics (SSOS) for Stateflow, starting from an existing structural operational semantics (SOS), and show the preservation of invariant properties between the two. We define bounded invariant checking for STS over symbolic configurations as a satisfiability problem. We develop an automated procedure for generating the initial and next-state predicates of the STS, and a prototype implementation of the technique in the form of a tool utilising standard, off-the-shelf satisfiability solvers. Finally, we present preliminary performance results by applying our tool on an illustrative example and two industrial models. 

Place, publisher, year, edition, pages
Open Publishing Association, 2022
Keywords
Computer programming languages, Formal verification, Model checking, Semantics, Simulink, Bounded model checking, Complex software, Invariant checking, Invariant properties, Safety critical software, Software modeling, STATEFLOW, Stateflow models, Structural operational semantics, Symbolic Transition Systems, Accident prevention
National Category
Computer Sciences
Identifiers
urn:nbn:se:kth:diva-328152 (URN)10.4204/EPTCS.371.3 (DOI)001048896900006 ()2-s2.0-85139852926 (Scopus ID)
Conference
4th International Workshop on Formal Methods for Autonomous Systems, FMAS 2022 and 4th International Workshop on Automated and Verifiable Software sYstem DEvelopment, ASYDE 2022, 26-27 September 2022
Note

QC 20230607

Available from: 2023-06-07 Created: 2023-06-07 Last updated: 2023-09-01Bibliographically approved
Amilon, J., Lidström, C. & Gurov, D. (2022). Deductive Verification Based Abstraction for Software Model Checking. In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics): . Paper presented at 11th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2022, Rhodes, Greece, 22-30 October 2022 (pp. 7-28). Springer Nature, 13701 LNCS
Open this publication in new window or tab >>Deductive Verification Based Abstraction for Software Model Checking
2022 (English)In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Springer Nature , 2022, Vol. 13701 LNCS, p. 7-28Conference paper, Published paper (Refereed)
Abstract [en]

The research community working on formal software verification has historically evolved into two main camps, grouped around two verification methods that are typically referred to as Deductive Verification and Model Checking. In this paper, we present an approach that applies deductive verification to formally justify abstract models for model checking in the TLA framework. We present a proof-of-concept tool chain for C programs, based on Frama-C for deductive verification and TLA+ for model checking. As a theoretical foundation, we summarise a previously developed abstract contract theory as a framework for combining these two methods. Since the contract theory adheres to the principles of contract based design, this justifies the use of the approach in a real-world system design setting. We evaluate our approach on two case studies: a simple C program simulating opening and closing of files, as well as a C program based on real software from the automotive industry.

Place, publisher, year, edition, pages
Springer Nature, 2022
Keywords
Contracts, Deductive verification, Model checking
National Category
Computer Sciences
Identifiers
urn:nbn:se:kth:diva-329628 (URN)10.1007/978-3-031-19849-6_2 (DOI)2-s2.0-85142704037 (Scopus ID)
Conference
11th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2022, Rhodes, Greece, 22-30 October 2022
Note

QC 20230622

Available from: 2023-06-22 Created: 2023-06-22 Last updated: 2024-03-15Bibliographically approved
Munoz, D.-J. -., Pinto, M., Gurov, D. & Fuentes, L. (2022). Defining categorical reasoning of numerical feature models with feature-wise and variant-wise quality attributes. In: 26th ACM International Systems and Software Product Line Conference, SPLC 2022 - Proceedings: . Paper presented at 26th ACM International Systems and Software Product Line Conference, ASPLC 2022, 12-16 September 2022 (pp. 132-139). Association for Computing Machinery (ACM)
Open this publication in new window or tab >>Defining categorical reasoning of numerical feature models with feature-wise and variant-wise quality attributes
2022 (English)In: 26th ACM International Systems and Software Product Line Conference, SPLC 2022 - Proceedings, Association for Computing Machinery (ACM) , 2022, p. 132-139Conference paper, Published paper (Refereed)
Abstract [en]

Automatic analysis of variability is an important stage of Software Product Line (SPL) engineering. Incorporating quality information into this stage poses a significant challenge. However, quality-aware automated analysis tools are rare, mainly because in existing solutions variability and quality information are not unified under the same model. In this paper, we make use of the Quality Variability Model (QVM), based on Category Theory (CT), to redefine reasoning operations. We start defining and composing the six most common operations in SPL, but now as quality-based queries, which tend to be unavailable in other approaches. Consequently, QVM supports interactions between variant-wise and feature-wise quality attributes. As a proof of concept, we present, implement and execute the operations as lambda reasoning for CQL IDE - the state-of-the-art CT tool. 

Place, publisher, year, edition, pages
Association for Computing Machinery (ACM), 2022
Keywords
automated reasoning, category theory, extended feature model, numerical features, quality attribute, Extended feature models, Feature models, Quality attributes, Quality information, Quality variability, Software Product Line, Variability modeling, Quality control
National Category
Computer Sciences
Identifiers
urn:nbn:se:kth:diva-328122 (URN)10.1145/3503229.3547057 (DOI)2-s2.0-85139107194 (Scopus ID)
Conference
26th ACM International Systems and Software Product Line Conference, ASPLC 2022, 12-16 September 2022
Note

QC 20230602

Available from: 2023-06-02 Created: 2023-06-02 Last updated: 2023-06-02Bibliographically approved
Gurov, D., Goranko, V. & Lundberg, E. (2022). Knowledge-based strategies for multi-agent teams playing against Nature. Artificial Intelligence, 309, 103728, Article ID 103728.
Open this publication in new window or tab >>Knowledge-based strategies for multi-agent teams playing against Nature
2022 (English)In: Artificial Intelligence, ISSN 0004-3702, E-ISSN 1872-7921, Vol. 309, p. 103728-, article id 103728Article in journal (Refereed) Published
Abstract [en]

We study teams of agents that play against Nature towards achieving a common objective. The agents are assumed to have imperfect information due to partial observability, and have no communication during the play of the game. We propose a natural notion of higher-order knowledge of agents. Based on this notion, we define a class of knowledgebased strategies, and consider the problem of synthesis of strategies of this class. We introduce a multi-agent extension, MKBSC, of the well-known knowledge-based subset construction applied to such games. Its iterative applications turn out to compute higherorder knowledge of the agents. We show how the MKBSC can be used for the design of knowledge-based strategy profiles, and investigate the transfer of existence of such strategies between the original game and in the iterated applications of the MKBSC, under some natural assumptions. We also relate and compare the "intensional" view on knowledge-based strategies based on explicit knowledge representation and update, with the "extensional" view on finite memory strategies based on finite transducers and show that, in a certain sense, these are equivalent.

Place, publisher, year, edition, pages
Elsevier BV, 2022
Keywords
Multi-agent games, Imperfect information, Higher-order knowledge, Knowledge-based strategies, Strategy synthesis, Dec-POMDP
National Category
Control Engineering
Identifiers
urn:nbn:se:kth:diva-314852 (URN)10.1016/j.artint.2022.103728 (DOI)000805237900002 ()2-s2.0-85130318766 (Scopus ID)
Note

QC 20220627

Available from: 2022-06-27 Created: 2022-06-27 Last updated: 2022-06-27Bibliographically approved
Ahrendt, W., Gurov, D., Johansson, M. & Rümmer, P. (2022). TriCo—Triple Co-piloting of Implementation, Specification and Tests. In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics): . Paper presented at 11th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2022, Rhodes, Greece, 22-30 October 2022 (pp. 174-187). Springer Nature, 13701 LNCS
Open this publication in new window or tab >>TriCo—Triple Co-piloting of Implementation, Specification and Tests
2022 (English)In: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Springer Nature , 2022, Vol. 13701 LNCS, p. 174-187Conference paper, Published paper (Refereed)
Abstract [en]

This white paper presents the vision of a novel methodology for developing safety-critical software, which is inspired by late developments in learning based co-piloting of implementations. The methodology, called TriCo, integrates formal methods with learning based approaches to co-pilot the agile, simultaneous development of three artefacts: implementation, specification, and tests. Whenever the user changes any of these, a TriCo empowered IDE would suggest changes to the other two artefacts in such a way that the three are kept consistent. The user has the final word on whether the changes are accepted, rejected, or modified. In the latter case, consistency will be checked again and re-established. We discuss the emerging trends which put the community in a good position to realise this vision, describe the methodology and workflow, as well as challenges and possible solutions for the realisation of TriCo.

Place, publisher, year, edition, pages
Springer Nature, 2022
National Category
Computer Sciences
Identifiers
urn:nbn:se:kth:diva-329625 (URN)10.1007/978-3-031-19849-6_11 (DOI)2-s2.0-85142769599 (Scopus ID)
Conference
11th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2022, Rhodes, Greece, 22-30 October 2022
Note

QC 20230622

Available from: 2023-06-22 Created: 2023-06-22 Last updated: 2023-06-22Bibliographically approved
Organisations
Identifiers
ORCID iD: ORCID iD iconorcid.org/0000-0002-0074-8786

Search in DiVA

Show all publications