Change search
Refine search result
1 - 37 of 37
CiteExportLink to result list
Permanent link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf
Rows per page
  • 5
  • 10
  • 20
  • 50
  • 100
  • 250
Sort
  • Standard (Relevance)
  • Author A-Ö
  • Author Ö-A
  • Title A-Ö
  • Title Ö-A
  • Publication type A-Ö
  • Publication type Ö-A
  • Issued (Oldest first)
  • Issued (Newest first)
  • Created (Oldest first)
  • Created (Newest first)
  • Last updated (Oldest first)
  • Last updated (Newest first)
  • Standard (Relevance)
  • Author A-Ö
  • Author Ö-A
  • Title A-Ö
  • Title Ö-A
  • Publication type A-Ö
  • Publication type Ö-A
  • Issued (Oldest first)
  • Issued (Newest first)
  • Created (Oldest first)
  • Created (Newest first)
  • Last updated (Oldest first)
  • Last updated (Newest first)
Select
The maximal number of hits you can export is 250. When you want to export more records please use the 'Create feeds' function.
  • 1.
    Aktug, Irem
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS. KTH, School of Electrical Engineering (EES), Centres, ACCESS Linnaeus Centre.
    Dam, Mads
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS. KTH, School of Electrical Engineering (EES), Centres, ACCESS Linnaeus Centre.
    Gurov, Dilian
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Provably Correct Runtime Monitoring2009In: Journal of Logic and Algebraic Programming, ISSN 1567-8326, E-ISSN 1873-5940, Vol. 78, no 5, 304-339 p.Article in journal (Refereed)
    Abstract [en]

    Runtime monitoring is an established technique to enforce a wide range of program safety and security properties. We present a formalization of monitoring and monitor inlining, for the Java Virtual Machine. Monitors are security automata given in a special-purpose monitor specification language, ConSpec. The automata operate on finite or infinite strings of calls to a fixed API, allowing local dependencies on parameter values and heap content. We use a two-level class file annotation scheme to characterize two key properties: (i) that the program is correct with respect to the monitor as a constraint on allowed program behavior, and (ii) that the program has a copy of the given monitor embedded into it. As the main application of these results we sketch a simple inlining algorithm and show how the two-level annotations can be completed to produce a fully annotated program which is valid in the standard sense of Floyd/Hoare logic. This establishes the mediation property that inlined programs are guaranteed to adhere to the intended policy. Furthermore, validity can be checked efficiently using a weakest precondition based annotation checker, thus preparing the ground for on-device checking of policy adherence in a proof-carrying code setting.

  • 2.
    Aktug, Irem
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Dam, Mads
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Gurov, Dilian
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Provably correct runtime monitoring (extended abstract)2008In: Fm 2008: Formal Methods, Proceedings / [ed] Cuellar, J; Maibaum, T; Sere, K, 2008, Vol. 5014, 262-277 p.Conference paper (Refereed)
    Abstract [en]

    Runtime monitoring is an established technique for enforcing a wide range of program safety and security properties. We present a formalization of monitoring and monitor inlining, for the Java Virtual Machine. Monitors are security automata given in a special-purpose monitor specification language, ConSpec. The automata operate on finite or infinite strings of calls to a fixed API, allowing local dependencies on parameter values and heap content. We use a two-level class file annotation scheme to characterize two key properties: (i) that the program is correct with respect to the monitor as a constraint on allowed program behavior, and (ii) that the program has an instance of the given monitor embedded into it, which yields state changes at prescribed points according to the monitor's transition function. As our main application of these results we describe a concrete inliner, and use the annotation scheme to characterize its correctness. For this inliner, correctness of the level II annotations can be decided efficiently by a weakest precondition annotation checker, thus allowing on-device checking of inlining correctness in a proof-carrying code setting.

  • 3.
    Aktug, Irem
    et al.
    KTH, School of Computer Science and Communication (CSC), Numerical Analysis and Computer Science, NADA.
    Gurov, Dilian
    KTH, School of Computer Science and Communication (CSC), Numerical Analysis and Computer Science, NADA.
    State Space Representation for Verification of Open Systems2006In: Algebraic Methodology And Software Technology, Proceedings / [ed] Johnson, M; Vene, V, Berlin: Springer , 2006, 5-20 p.Conference paper (Refereed)
    Abstract [en]

    When designing an open system, there might be no implementation available for certain components at verification time. For such systems, verification has to be based on assumptions on the underspecified components. When component assumptions are expressed in Hennessy-Milner logic (HML), the state space of open systems can be naturally represented with modal transition systems (NITS), a graphical specification language equiexpressive with HML. Having an explicit state space representation supports state space exploration based verification techniques, Besides, it enables proof reuse and facilitates visualization for the user guiding the verification process. in interactive verification. As an intuitive representation of system behavior, it aids debugging when proof generation fails in automatic verification.

    However, HML is not expressive enough to capture temporal assumptions. For this purpose, we extend MTSs to represent the state space of open systems where component assumptions are specified in modal mu-calculus. We present a two-phase construction from process algebraic open system descriptions to such state space representations. The first phase deals with component assumptions, and is essentially a maximal model construction for the modal p-calculus. In the second phase, the models obtained are combined according to the structure of the open system to form the complete state space. The construction is sound and complete for systems with a single unknown component and sound for those-without dynamic process creation. For establishing open system properties based on the representation, we present a proof system which is sound and complete for prime formulae.

  • 4.
    Aktug, Irem
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Gurov, Dilian
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Towards State Space Exploration Based Verification of Open Systems2005In: 4th International Workshop on Automated Verification of Infinite-State Systems (AVIS’05), April 2005, Edinburgh, Scotland, 2005Conference paper (Refereed)
  • 5.
    Amighi, Afshin
    et al.
    University of Twente.
    de Carvalho Gomes, Pedro
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Gurov, Dilian
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Huisman, Marieke
    University of Twente.
    Provably Correct Control Flow Graphs from Java Bytecode Programs with Exceptions2015In: International Journal on Software Tools for Technology Transfer (STTT), ISSN 1433-2779, E-ISSN 1433-2787, ISSN 1433-2779Article in journal (Refereed)
    Abstract [en]

    We present an algorithm for extracting control flow graphs from Java bytecode that captures normal as well as exceptional control flow. We prove its correctness, in the sense that the behaviour of the extracted control flow graph is a sound over-approximation of the behaviour of the original program. This makes control flow graphs suitable for performing various static analyses, such as model checking of temporal safety properties.Analyzing exceptional control flow for Java bytecode is difficult because of the stack-based nature of the language. We therefore develop the extraction in two stages. In the first, we abstract away from the complications arising from exceptional flows, and relativize the extraction on an oracle that is able to look into the stack and predict the exceptions that can be raised at each instruction. This idealized algorithm provides a specification for concrete extraction algorithms, which have to provide a suitable implementation for the oracle. We prove correctness of the idealized algorithm by means of behavioural simulation.In the second stage, we develop a concrete extraction algorithm that consists of two phases. In the first phase, the program is transformed into a BIR program, a stack-less intermediate representation of Java bytecode, from which the control flow graph is extracted in the second phase. We use this intermediate format because it provides the information needed to implement the oracle, and since it gives rise to more compact graphs. We show that the behaviour of the control flow graph extracted via the intermediate representation is a sound over-approximation of the behaviour of the graph extracted by the direct, idealized algorithm, and thus of the original program. The concrete extraction algorithm is implemented as the ConFlEx tool. A number of test cases are performed to evaluate the efficiency of the algorithm.

  • 6.
    Amighi, Afshin
    et al.
    University of Twente.
    de Carvalho Gomes, Pedro
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Gurov, Dilian
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Huisman, Marieke
    University of Twente.
    Provably Correct Control-Flow Graphs from Java Programs with Exceptions2012Report (Other academic)
    Abstract [en]

    We present an algorithm to extract flow graphs from Java bytecode, including exceptional control flows. We prove its correctness, meaning that the behavior of the extracted control-flow graph is a sound over-approximation of the behavior of the original program. Thus any safety property that holds for the extracted control-flow graph also holds for the original program. This makes control-flow graphs suitable for performing various static analyses, such as model checking.The extraction is performed in two phases. In the first phase the program is transformed into a BIR program, a stack-less intermediate representation of Java bytecode, from which the control-flow graph is extracted in the second phase. We use this intermediate format because it results in compact flow graphs, with provably correct exceptional control flow. To prove the correctness of the two-phase extraction, we also define an idealized extraction algorithm, whose correctness can be proven directly. Then we show that the behavior of the control-flow graph extracted via the intermediate representation is an over-approximation of the behavior of the directly extracted graphs, and thus of the original program. We implemented the indirect extraction as the CFGEx tool and performed several test-cases to show the efficiency of the algorithm.

  • 7.
    Amighi, Afshin
    et al.
    University of Twente.
    de Carvalho Gomes, Pedro
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Gurov, Dilian
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Huisman, Marieke
    University of Twente.
    Sound Control-Flow Graph Extraction for Java Programs with Exceptions2012In: Software Engineering and Formal Methods: 10th International Conference, SEFM 2012, Thessaloniki, Greece, October 1-5, 2012. Proceedings, Springer Berlin/Heidelberg, 2012, 33-47 p.Conference paper (Refereed)
    Abstract [en]

    We present an algorithm to extract control-flow graphs from Java bytecode, considering exceptional flows. We then establish its correctness: the behavior of the extracted graphs is shown to be a sound over-approximation of the behavior of the original programs. Thus, any temporal safety property that holds for the extracted control-flow graph also holds for the original program. This makes the extracted graphs suitable for performing various static analyses, in particular model checking. The extraction proceeds in two phases. First, we translate Java bytecode into BIR, a stack-less intermediate representation. The BIR transformation is developed as a module of Sawja, a novel static analysis framework for Java bytecode. Besides Sawja’s efficiency, the resulting intermediate representation is more compact than the original bytecode and provides an explicit representation of exceptions. These features make BIR a natural starting point for sound control-flow graph extraction. Next, we formally define the transformation from BIR to control-flow graphs, which (among other features) considers the propagation of uncaught exceptions within method calls. We prove the correctness of the two-phase extraction by suitably combining the properties of the two transformations with those of an idealized control-flow graph extraction algorithm, whose correctness has been proved directly. The control-flow graph extraction algorithm is implemented in the ConFlEx tool. A number of test-cases show the efficiency and the utility of the implementation.

  • 8.
    Bakhshi, Rana
    et al.
    KTH, School of Information and Communication Technology (ICT).
    Gurov, Dilian
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Verification of Peer-to-peer Algorithms: A Case Study2007In: Electronical Notes in Theoretical Computer Science, ISSN 1571-0661, E-ISSN 1571-0661, Vol. 181, no 1, 35-47 p.Article in journal (Refereed)
    Abstract [en]

    The problem of maintaining structured peer-to-peer (P2P) overlay networks in the presence of concurrent joins and failures of nodes is the subject of intensive research. The various algorithms underlying P2P systems are notoriously difficult to design and analyse. Thus, when verifying P2P algorithms, a real challenge is to find an adequate level of abstraction at which to model the algorithms and perform the verifications. In this paper, we propose an abstract model for structured P2P networks with ring topology. Our model is based on process algebra, which, with its well-developed theory, provides the right level of abstraction for the verification of many basic P2P algorithms. As a case study, we verify the correctness of the stabilization algorithm of Chord, one of the best-known P2P overlay networks. To show the correctness of the algorithm, we provide a specification and an implementation of the Chord system in process algebra and establish bisimulation equivalence between the two.

  • 9. Borgström, Johannes
    et al.
    Nestmann, Uwe
    Onana, Luc Alima
    KTH, School of Information and Communication Technology (ICT), Microelectronics and Information Technology, IMIT.
    Gurov, Dilian
    KTH, School of Information and Communication Technology (ICT), Microelectronics and Information Technology, IMIT.
    Verifying a structured peer-to-peer overlay network: The static case2005In: GLOBAL COMPUTING, 2005, Vol. 3267, 250-265 p.Conference paper (Refereed)
    Abstract [en]

    Structured peer-to-peer overlay networks are a class of algorithms that provide efficient message routing for distributed applications using a sparsely connected communication network. In this paper, we formally verify a typical application running on a fixed set of nodes. This work is the foundation for studies of a more dynamic system. We identify a value and expression language for a value-passing CCS that allows us to formally model a distributed hash table implemented over a static DKS overlay network. We then provide a specification of the lookup operation in the same language, allowing us to formally verify the correctness of the system in terms of observational equivalence between implementation and specification. For the proof, we employ an abstract notation for reachable states that allows us to work conveniently up to structural congruence, thus drastically reducing the number and shape of states to consider. The structure and techniques of the correctness proof are reusable for other overlay networks.

  • 10.
    Dam, Mads
    et al.
    KTH, Superseded Departments, Microelectronics and Information Technology, IMIT.
    Gurov, Dilian
    mu-calculus with explicit points and approximations2002In: Journal of logic and computation (Print), ISSN 0955-792X, E-ISSN 1465-363X, Vol. 12, no 2, 255-269 p.Article in journal (Refereed)
    Abstract [en]

    We present a Gentzen-style sequent calculus for program verification which accommodates both model checking-like verification based on global state space exploration, and compositional reasoning. To handle the complexities arising from the presence of fixed-point formulas, programs with dynamically evolving architecture, and cut rules we use transition assertions, and introduce fixed-point approximants explicitly into the assertion language. We address, in a game-based manner, the semantical basis of this approach, as it applies to the entailment subproblem. Soundness and completeness results are obtained, and examples are shown illustrating some of the concepts.

  • 11.
    De Carvalho Gomes, Pedro
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Gurov, Dilian
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Huisman, M.
    Specification and verification of synchronization with condition variables2017In: 5th International Workshop on Formal Techniques for Safety-Critical Systems, FTSCS 2016, Springer, 2017, Vol. 694, 3-19 p.Conference paper (Refereed)
    Abstract [en]

    In this paper we propose a technique to specify and verify the correct synchronization of concurrent programs with condition variables. We define correctness as the liveness property: “every thread synchronizing under a set of condition variables eventually exits the synchronization”, under the assumption that every such thread eventually reaches its synchronization block. Our technique does not avoid the combinatorial explosion of interleavings of thread behaviors. Instead, we alleviate it by abstracting away all details that are irrelevant to the synchronization behavior of the program, which is typically significantly smaller than its overall behavior. First, we introduce SyncTask, a simple imperative language to specify parallel computations that synchronize via condition variables. We consider a SyncTask program to have a correct synchronization iff it terminates. Further, to relieve the programmer from the burden of providing specifications in SyncTask, we introduce an economic annotation scheme for Java programs to assist the automated extraction of SyncTask programs capturing the synchronization behavior of the underlying program. We prove that every Java program annotated according to the scheme (and satisfying the assumption) has a correct synchronization iff its corresponding SyncTask program terminates. We show how to transform the verification of termination into a standard reachability problem over Colored Petri Nets that is efficiently solvable by existing Petri Net analysis tools. Both the SyncTask program extraction and the generation of Petri Nets are implemented in our STaVe tool. We evaluate the proposed framework on a number of test cases as a proof-of-concept.

  • 12.
    de Carvalho Gomes, Pedro
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Gurov, Dilian
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Huisman, Marieke
    University of Twente.
    Algorithmic Verification of Synchronization with Condition Variables2015Report (Other academic)
    Abstract [en]

    Condition variables are a common synchronization mechanism present in many programming languages. Still, due to the combinatorial complexity of the behaviours the mechanism induces, it has not been addressed sufficiently with formal techniques. In this paper we propose a fully automated technique to prove the correct synchronization of concurrent programs synchronizing via condition variables, where under correctness we mean the liveness property: "If for every set of condition variables, every thread synchronizing under the variables of the set eventually enters its synchronization block, then every thread will eventually exit the synchronization".First, we introduce SyncTask, a simple imperative language to specify parallel computations that synchronize via condition variables. Next, we model the constructs of the language as Petri Net components, and define rules to extract and compose nets from a SyncTask program. We show that a SyncTask program terminates if and only if the corresponding Petri Net always reaches a particular final marking. We thus transform the verification of termination into a reachability problem on the net, which can be solved efficiently by existing Petri Net analysis tools. Further, to relieve the programmer from the burden of having to provide specifications in SyncTask, we introduce an economic annotation scheme for Java programs to assist the automated extraction of SyncTask programs capturing the synchronization behaviour of the underlying program. We show that, for the Java programs that can be annotated according to the scheme, the above-mentioned liveness property holds if and only if the corresponding SyncTask program terminates. Both the SyncTask program extraction and the generation of Petri Nets are implemented in the STaVe tool. We evaluate the proposed verification framework on a number of test cases

  • 13.
    de Carvalho Gomes, Pedro
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Picoco, Attilio
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS. Polytechnic University of Turin.
    Gurov, Dilian
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Sound Control Flow Graph Extraction from Incomplete Java Bytecode Programs2014In: Fundamental Approaches to Software Engineering: 17th International Conference, FASE 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014, Proceedings / [ed] Stefania Gnesi and Arend Rensink, Springer Berlin/Heidelberg, 2014, 215-229 p.Conference paper (Refereed)
    Abstract [en]

    The modular analysis of control flow of incompleteJava bytecode programs is challenging, mainly because of the complex semantics of the language,and the unknown inter-dependencies between the available and unavailable components.In this paper we describe a technique for incremental, modular extraction ofcontrol flow graphs that are provably sound w.r.t.~sequences of method invocations and exceptions.The extracted models are suitable for various program analyses,in particular model-checking of temporal control flow safety properties.Soundness comes at the price of over-approximation,potentially giving rise to false positives reports during verification.Still, our technique supports incremental refinement of the already extracted models,as more components code becomes available.The extraction has been implemented as the ConFlex tool, and test-cases show its utility and efficiency.

  • 14.
    de Carvalho Gomes, Pedro
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Picoco, Attilio
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Gurov, Dilian
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Sound Extraction of Control-Flow Graphs from open Java Bytecode Systems2012Report (Other academic)
    Abstract [en]

    Formal verification techniques have been widely deployed as means to ensure the quality of software products. Unfortunately, they suffer with the combinatorial explosion of the state space. That is, programs have a large number of states, sometimes infinite. A common approach to alleviate the problem is to perform the verification over abstract models from the program. Control-flow graphs (CFG) are one of the most common models, and have been widely studied in the past decades. Unfortunately, previous works over modern programming languages, such as Java, have either neglected features that influence the control-flow, or do not provide a correctness argument about the CFG construction. This is an unbearable issue for formal verification, where soundness of CFGs is a mandatory condition for the verification of safety-critical properties. Moreover, one may want to extract CFGs from the available components of an open system. I.e., a system whose at least one of the components is missing. Soundness is even harder to achieve in this scenario, because of the unknown inter-dependences between software components.

    In the current work we present a framework to extract control-flow graphs from open Java Bytecode systems in a modular fashion. Our strategy requires the user to provide interfaces for the missing components. First, we present a formal definition of open Java bytecode systems. Next, we generalize a previous algorithm that performs the extraction of CFGs for closed programs to a modular set-up. The algorithm uses the user-provided interfaces to resolve inter-dependences involving missing components. Eventually the missing components will arrive, and the open system will become closed, and can execute. However, the arrival of a component may affect the soundness of CFGs which have been extracted previously. Thus, we define a refinement relation, which is a set of constraints upon the arrival of components, and prove that the relation guarantees the soundness of CFGs extracted with the modular algorithm. Therefore, the control-flow safety properties verified over the original CFGs still hold in the refined model.

    We implemented the modular extraction framework in the ConFlEx tool. Also, we have implemented the reusage from previous extractions, to enable the incremental extraction of a newly arrived component. Our technique performs substantial over-approximations to achieve soundness. Despite this, our test cases show that ConFlEx is efficient. Also, the extraction of the CFGs gets considerable speed-up by reusing results from previous analyses.

  • 15.
    Guanciale, Roberto
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Gurov, Dilian
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Privacy preserving business process fusion2015In: International Workshops on Business Process Management Workshops, BPM 2014, Springer, 2015, Vol. 202, 96-101 p.Conference paper (Refereed)
    Abstract [en]

    Virtual enterprises (VEs) are temporary and loosely coupled alliances of businesses that join their skills to catch new business opportunities. However, the dependencies among the activities of a prospective VE cross the boundaries of the VE constituents. It is therefore crucial to allow the VE constituents to discover their local views of the interorganizational workflow, enabling each company to re-shape, optimize and analyze the possible local flows that are consistent with the processes of the other VE constituents. We refer to this problem asVE process fusion. Even if it has been widely investigated, no previous work addresses VE process fusion in the presence of privacy constraints. In this paper we demonstrate how private intersection of regular languages can be used as the main building block to implement the privacy preserving fusion of business processes modeled by means of bounded Petri nets.

  • 16.
    Guanciale, Roberto
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Gurov, Dilian
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Laud, P.
    Business process engineering and secure multiparty computation2015In: Cryptology and Information Security Series, ISSN 1871-6431, Vol. 13, 129-149 p.Article in journal (Refereed)
    Abstract [en]

    In this chapter we use secure multiparty computation (SMC) to enable privacy-preserving engineering of inter-organizational business processes. Business processes often involve structuring the activities of several organizations, for example when several potentially competitive enterprises share their skills to form a temporary alliance. One of the main obstacles to engineering the processes that govern such collaborations is the perceived threat to the participants’ autonomy. In particular, the participants can be reluctant to expose their internal processes or logs, as this knowledge can be analyzed by other participants to reveal sensitive information. We use SMC techniques to handle two problems in this context: process fusion and log auditing. Process fusion enables the constituents of a collaboration to discover their local views of the inter-organizational workflow, enabling each company to re-shape, optimize and analyze their local flows. Log auditing enables a participant that owns a business process to check if the partner’s logs match its business process, thus enabling the two partners to discover failures, errors and inefficiencies.

  • 17.
    Guanciale, Roberto
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Gurov, Dilian
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Laud, Peeter
    Private intersection of regular languages2014In: Privacy, Security and Trust (PST), 2014 Twelfth Annual International Conference on / [ed] Ali Miri, Urs Hengartner, Nen-Fu Huang, Audun Jøsang, Joaquín García-Alfaro, IEEE conference proceedings, 2014, 112-120 p.Conference paper (Refereed)
    Abstract [en]

    This paper addresses the problem of computing the intersection of regular languages in a privacy-preserving fashion. Private set intersection has been addressed earlier in the literature, but for finite sets only. We discuss the various possibilities for solving the problem efficiently, and argue for an approach based on minimal deterministic finite automata (DFA) as a suitable, non-leaking representation of regular language intersection. We propose two different algorithms for DFA minimization in a secure multiparty computation setting, illustrating different aspects of programming based on universal composability and the constraints this sets on existing algorithms. The implementation of our algorithms is based on the programming language SECREC, executing on the SHAREMIND platform for secure multiparty computation. As one application domain we consider fusion of virtual enterprise business processes.

  • 18.
    Gurov, Dilian
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Havelund, Klaus
    Huisman, Marieke
    Monahan, Rosemary
    Static and Runtime Verification, Competitors or Friends?: (Track Summary)2016In: LEVERAGING APPLICATIONS OF FORMAL METHODS, VERIFICATION AND VALIDATION: FOUNDATIONAL TECHNIQUES, PT I, 2016, 397-401 p.Conference paper (Refereed)
  • 19.
    Gurov, Dilian
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Huisman, Marieke
    Interface abstraction for compositional verification2005In: SEFM 2005: Third IEEE International Conference on Software Engineering and Formal Methods, Proceedings / [ed] Aichernig, BK; Beckert, B, 2005, 414-423 p.Conference paper (Refereed)
    Abstract [en]

    To support dynamic loading of applications on portable devices, one needs compositional reasoning techniques to ensure that newly loaded applications cannot break the overall security of a device. In earlier work, we developed an algorithmic verification technique for control flow based safety properties of smart card applications, which allows global system properties to be inferred from the properties of the components. Application of the technique requires knowledge of the names of all methods implemented by these components. In a truly compositional setting, however, one only knows the public interface of the new applet and does not have access to any implementation details. To compositionally verify interface properties of applets, one therefore has to combine our verification technique with an abstraction which preserves the interface behaviour and reduces the set of implemented methods to the set of public methods. In this paper we develop such an abstraction technique: we formally define the notion of interface behaviour and propose an inlining transformation which we prove to preserve the interface properties expressible in our specification language. In addition, we show on a concrete case study how the reduction in the number of methods resulting from the interface abstraction drastically improves the performance of the computationally most expensive step of the compositional verification technique.

  • 20.
    Gurov, Dilian
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Huisman, Marieke
    University of Twente, Netherlands .
    Reducing behavioural to structural properties of programs with procedures2013In: Theoretical Computer Science, ISSN 0304-3975, E-ISSN 1879-2294, Vol. 480, 69-103 p.Article in journal (Refereed)
    Abstract [en]

    There is an intimate link between program structure and behaviour. Exploiting this link to phrase program correctness problems in terms of the structural properties of a program graph rather than in terms of its unfoldings is a useful strategy for making analyses more tractable. The present paper presents a characterisation of behavioural program properties through sets of structural properties by means of a translation. The characterisation is given in the context of a program model based on control flow graphs of sequential programs with procedures, abstracting away completely from program data, and properties expressed in a fragment of the modal mu-calculus with boxes and greatest fixed-points only. The property translation is based on a tableau construction that conceptually amounts to symbolic execution of the behavioural formula, collecting structural constraints along the way. By keeping track of the subformulae that have been examined, recursion in the structural constraints can be identified and captured by fixed-point formulae. The tableau construction terminates, and the characterisation is exact, i.e., the translation is sound and complete. A prototype implementation has been developed. In addition, we show how the translation can be extended beyond the basic flow graph model and safety logic to richer behavioural models (such as open programs) and richer program models (including Boolean programs), and discuss possible extensions for more complex logics. We present several applications of the characterisation, in particular sound and complete compositional verification for behavioural properties based on maximal models.

  • 21.
    Gurov, Dilian
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Huisman, Marieke
    University of Twente, Netherlands.
    Reducing Behavioural to Structural Properties of Programs with Procedures2009In: VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION / [ed] Jones ND; MullerOlm M, 2009, Vol. 5403, 136-150 p.Conference paper (Refereed)
    Abstract [en]

    There is an intimate link between program structure and behaviour. Exploiting this link to phrase program correctness problems in terms of the structural properties of a program graph rather than in terms of its unfoldings is a useful strategy for making analyses more tractable. This paper presents a characterisation of behavioural program properties through sets of structural properties by means of a translation. The characterisation is given in the context of a program model based on control flow graphs of sequential programs with possibly recursive procedures, and properties expressed in a fragment of the modal mu-calculus with boxes and greatest fixed-points only. The property translation is based on a tableau construction that conceptually amounts to symbolic execution of the behavioural formula, collecting structural constraints along the way. By keeping track of the subformulae that have been examined, recursion in the structural constraints can be identified and captured by fixed-point formulae. The tableau construction terminates, and the characterisation is exact, i.e., the translation is sound and complete. A prototype implementation has been developed. We discuss several applications of the characterisation, in particular compositional verification for behavioural properties, based on maximal models.

  • 22.
    Gurov, Dilian
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Huisman, Marieke
    Sprenger, Christoph
    Compositional verification of sequential programs with procedures2008In: Information and Computation, ISSN 0890-5401, E-ISSN 1090-2651, Vol. 206, no 7, 840-868 p.Article in journal (Refereed)
    Abstract [en]

    We present a method for algorithmic, compositional verification of control-flow-based safety properties of sequential programs with procedures. The application of the method involves three steps: (1) decomposing the desired global property into local properties of the components, (2) proving the correctness of the property decomposition by using a maximal model construction, and (3) verifying that the component implementations obey their local specifications. We consider safety properties of both the structure and the behaviour of program control flow. Our compositional verification method builds on a technique proposed by Grumberg and Long that uses maximal models to reduce compositional verification of finite-state parallel processes to standard model checking. We present a novel maximal model construction for the fragment of the modal P-calculus with boxes and greatest fixed points only, and adapt it to control-flow graphs modelling components described in a sequential procedural language. We extend our verification method to programs with private procedures by defining an abstraction, presented as an inlining transformation. All algorithms have been implemented in a tool set automating all required verification steps. We validate our approach on an electronic purse case study.

  • 23.
    Gurov, Dilian
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Laud, P.
    Guanciale, Roberto
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Privacy preserving business process matching2015In: 2015 13th Annual Conference on Privacy, Security and Trust, IEEE , 2015, 36-43 p.Conference paper (Refereed)
    Abstract [en]

    Business process matching is the activity of checking whether a given business process can interoperate with another one in a correct manner. In case the check fails, it is desirable to obtain information about how the first process can be corrected with as few modifications as possible to achieve interoperability. In case the two business processes belong to two separate enterprises that want to build a virtual enterprise, business process matching based on revealing the business processes poses a clear threat to privacy, as it may expose sensitive information about the inner operation of the enterprises. In this paper we propose a solution to this problem for business processes described by means of service automata. We propose a measure for similarity between service automata and use this measure to devise an algorithm that constructs the most similar automaton to the first one that can interoperate with the second one. To achieve privacy, we implement this algorithm in the programming language SecreC, executing on the Sharemind platform for secure multiparty computation. As a result, only the correction information is leaked to the first enterprise and no more.

  • 24.
    Gurov, Dilian
    et al.
    KTH, School of Computer Science and Communication (CSC).
    Markov, Minko
    Self-Correlation and Maximum Independence in Finite Relations2015In: Electronic Proceedings in Theoretical Computer Science, ISSN 2075-2180, E-ISSN 2075-2180, no 191, 60-74 p.Article in journal (Refereed)
    Abstract [en]

    We consider relations with no order on their attributes as in Database Theory. An independent partition of the set of attributes S of a finite relation R is any partition (sic) of S such that the join of the projections of R over the elements of (sic) yields R. Identifying independent partitions has many applications and corresponds conceptually to revealing orthogonality between sets of dimensions in multidimensional point spaces. A subset of S is termed self-correlated if there is a value of each of its attributes such that no tuple of R contains all those values. This paper uncovers a connection between independence and self-correlation, showing that the maximum independent partition is the least fixed point of a certain inflationary transformer alpha that operates on the finite lattice of partitions of S. alpha is defined via the minimal self-correlated subsets of S. We use some additional properties of alpha to show the said fixed point is still the limit of the standard approximation sequence, just as in Kleene's well-known fixed point theorem for continuous functions.

  • 25.
    Gurov, Dilian
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Østvold, B.M.
    Schaefer, I.
    A hierarchical variability model for software product lines2012In: Leveraging Applications of Formal Methods, Verification, and Validation: International Workshops, SARS 2011 and MLSC 2011, Held Under the Auspices of ISoLA 2011 in Vienna, Austria, October 17-18, 2011. Revised Selected Papers / [ed] Reiner Hähnle, Jens Knoop, Tiziana Margaria, Dietmar Schreiner, Bernhard Steffen, Springer, 2012, 181-199 p.Conference paper (Refereed)
    Abstract [en]

    A key challenge in software product line engineering is to represent solution space variability in an economic, yet easily understandable fashion. We introduce the notion of hierarchical variability models to describe families of products in a manner that facilitates their modular design and analysis. In this model, a family is represented by a common set of artifacts and a set of variation points with associated variants. A variant is again a hierarchical variability model, leading to a hierarchical structure. These models, however, are not unique with respect to the families they define. We therefore propose a quantitative measure on hierarchical variability models that expresses the degree to which a variability model captures commonality and variability in a family. Further, by imposing well-formedness constraints, we identify a class of variability models that, by construction, have maximal measure and are unique for the families they define. For this class of simple families, we provide a procedure that reconstructs their hierarchical variability model. The reconstructed model can be used to drive various static analyses by divide-and-conquer reasoning. Hierarchical variability models strike a balance between the formalism's expressiveness and the desirable property of model uniqueness. We illustrate the approach by a small product line of Java classes.

  • 26. Huisman, M.
    et al.
    Gurov, Dilian
    KTH.
    Sprenger, C.
    Chugunov, G.
    Checking absence of illicit applet interactions: A case study2004In: FUNDAMENTAL APPROACHES TO SOFTWARE ENGINEERING, PROCEEDINGS / [ed] Wermelinger, M; MargariaSteffen, T, BERLIN: SPRINGER , 2004, Vol. 2984, 84-98 p.Conference paper (Refereed)
    Abstract [en]

    This paper presents the use of a method - and its corresponding tool set - for compositional verification of applet interactions on a realistic industrial smart card case study. The case study, an electronic purse, is provided by smart card producer Gemplus as a test case for formal methods for smart cards. The verification method focuses on the possible interactions between different applets, co-existing on the same card, and provides a technique to specify and detect illicit interactions between these applets. The method is compositional, thus supporting post-issuance loading of applets. The correctness of a global system property can algorithmically be inferred from local applet properties. Later, when loading applets on a card, the implementations are matched against these local properties, in order to guarantee the global property. The theoretical framework underlying our method has been presented elsewhere; the present paper evaluates its practical usability by means of an industrial case study. In particular, we outline the tool set that we have assembled to support the verification process, combining existing model checkers with newly developed tools, tailored to our method.

  • 27. Huisman, Marieke
    et al.
    Aktug, Irem
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Gurov, Dilian
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Program Models for Compositional Verification2008In: FORMAL METHODS AND SOFTWARE ENGINEERING, PROCEEDINGS, Berlin: Springer , 2008, 147-166 p.Conference paper (Refereed)
    Abstract [en]

    Compositional verification is crucial for guaranteeing the security of systems where new components can be loaded dynamically. In earlier work, we developed a compositional verification principle for control-flow properties of sequential control flow graphs with procedures. This paper discusses how the principle can be generalised to richer program models. We first present a generic program model, of which the original program model is an instantiation, and explicate under what conditions the compositional verification principle applies. We then present two other example instantiations of the generic model: with exceptional and with multi-threaded control flow, and show that for these particular instantiations the conditions hold. The program models we present are specifically tailored to our compositional verification principle, however, they are sufficiently intuitive and standard to be useful on their own. Tool support and practical application of the method are discussed.

  • 28.
    Huisman, Marieke
    et al.
    INRIA Sophia Antipolis, France.
    Gurov, Dilian
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Composing Modal Properties of Programs with Procedures2009In: Electronical Notes in Theoretical Computer Science, ISSN 1571-0661, E-ISSN 1571-0661, Vol. 203, no 7, 87-101 p.Article in journal (Refereed)
    Abstract [en]

    In component based software design, formal reasoning about programs has to be compositional, allowing global, program-wide properties to be inferred from the properties of its components. The present paper addresses the problem of compositional verification of behavioural control flow properties of sequential programs with procedures, expressed in a modal logic. We use as a starting point a maximal model based method previously developed by the authors, which assumes the local properties to be structural (rather than behavioural). To handle local behavioural properties, we propose the combination of the above method with a translation from behavioural properties to sets of structural ones. The present paper presents a direct solution for the logic, and prepares the ground for a translation for the considerably more expressive logic obtained by adding greatest fixed-point recursion.

  • 29.
    Huisman, Marieke
    et al.
    Univ Twente, Enschede, Netherlands.
    Gurov, Dilian
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    CVPP: A Tool Set for Compositional Verification of Control-Flow Safety Properties2011In: FORMAL VERIFICATION OF OBLECT-ORIENTED SOFTWARE / [ed] Beckert, B; Marche, C, 2011, Vol. 6528, 107-121 p.Conference paper (Refereed)
    Abstract [en]

    This paper describes CVPP, a tool set for compositional verification of control-flow safety properties for programs with procedures. The compositional verification principle that underlies CVPP is based on maximal models constructed from component specifications. Maximal models replace the actual components when verifying the whole program, either for the purposes of modularity of verification or due to unavailability of the component implementations at verification time. A characteristic feature of the principle and the tool set is the distinction between program structure and behaviour. While behavioural properties are more abstract and convenient for specification purposes, structural ones are easier to manipulate, in particular when it comes to verification or the construction of maximal models. Therefore, CVPP also contains the means to characterise a given behavioural formula by a set of structural formulae. The paper presents the underlying framework for compositional verification and the components of the tool set. Several verification scenarios are described, as well as wrapper tools that support the automatic execution of such scenarios, providing appropriate pre- and post-processing to interface smoothly with the user and to encapsulate the inner workings of the tool set.

  • 30.
    Schaefer, Ina
    et al.
    Technische Universität Braunschweig, Germany.
    Gurov, Dilian
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Soleimanifard, Siavash
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Compositional Algorithmic Verification of Software Product Lines2010Conference paper (Refereed)
    Abstract [en]

    Software product line engineering allows large software systems to be developed and adapted for varying customer needs. The products of a software product line can be described by means of a {\em hierarchical variability model} specifying the commonalities and variabilities between the artifacts of the individual products. The number of products generated by a hierarchical model is exponential in its size, which poses a serious challenge to software product line analysis and verification. For an analysis technique to scale, the effort has to be linear in the size of the model rather than linear in the number of products it generates. Hence, efficient product line verification is only possible if {\em compositional} verification techniques are applied that allow the analysis of products to be {\em relativized}  on the properties of their variation points. In this paper, we propose simple hierarchical variability models (SHVM) with explicit variation points as a novel way to describe a set of products consisting of sets of methods. SHVMs provide a trade--off between expressiveness and a clean and simple model suitable for compositional verification. We generalize a previously developed  compositional technique and tool set for the automatic verification of control--flow based temporal safety properties to product lines defined by SHVMs, and prove soundness of the generalization. The desired property relativization is achieved by introducing variation point specifications. We evaluate the proposed technique on a number of test cases.

  • 31.
    Soleimanifard, Siavash
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Gurov, Dilian
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Algorithmic verification of procedural programs in the presence of code variability2015In: Formal Aspects of Component Software: 11th International Symposium, FACS 2014, Bertinoro, Italy, September 10-12, 2014, Revised Selected Papers, Springer, 2015, Vol. 8997, 41 p.327-345 p.Conference paper (Refereed)
    Abstract [en]

    We present a generic framework for verifying temporal safety properties of procedural programs that are dynamically or statically configured by replacing, adapting, or adding new components. To deal with such a variability of a program, we require programmers to provide local specifications for its variable components, and verify the global properties by replacing these specifications with maximal models. Our framework is a generalization of a previously developed framework that abstracts from all program data. In this work, we capture program data and thus significantly increase the range of properties that can be verified. Our framework is generic by being parametric on the set of observed program events and their semantics. We separate program structure from the behavior it induces to facilitate independent component specification and verification. We provide tool support for an instantiation of our framework to programs written in a procedural language with pointers as the only datatype.

  • 32.
    Soleimanifard, Siavash
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Gurov, Dilian
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Huisman, Marieke
    University of Twente.
    Procedure-Modular Specification and Verification of Temporal Safety Properties2013In: Software & Systems Modeling, ISSN 1619-1366Article in journal (Refereed)
    Abstract [en]

    This paper describes ProMoVer, a tool for fully automated procedure-modular verification of Java programs equipped with method-local and global assertions that specify safety properties of sequences of method invocations. Modularity at the procedure-level is a natural instantiation of the modular verification paradigm, where correctness of global properties is relativized on the local properties of the methods rather than on their implementations. Here, it is based on the construction of maximal models for a program model that abstracts away from program data. This approach allows global properties to be verified in the presence of code evolution, multiple method implementations (as arising from software product lines), or even unknown method implementations (as in mobile code for open platforms). ProMoVer automates a typical verification scenario for a previously developed tool set for compositional verification of control flow safety properties, and provides appropriate pre- and post-processing. Both linear-time temporal logic and finite automata are supported as formalisms for expressing local and global safety properties, allowing the user to choose a suitable format for the property at hand. Modularity is exploited by a mechanism for proof reuse that detects and minimizes the verification tasks resulting from changes in the code and the specifications. The verification task is relatively light-weight due to support for abstraction from private methods and automatic extraction of candidate specifications from method implementations. We evaluate the tool on a number of applications from the domains of Java Card and web-based application.

  • 33.
    Soleimanifard, Siavash
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Gurov, Dilian
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Huisman, Marieke
    University of Twente.
    Procedure-Modular Verification of Control Flow Safety Properties2010In: Proceedings of the 12th Workshop on Formal Techniques for Java-Like Programs, 2010Conference paper (Refereed)
    Abstract [en]

    This paper describes a novel technique for fully automated procedure–modular verification of Java programs equipped with method–local and global assertions that specify safety properties of sequences of method invocations. Modularity of verification is achieved by relativizing the correctness of global properties on the local properties rather than on the implementations of methods, and is based on the construction of maximal models. Tool support is provided by means of ProMoVer, a tool that is essentially a wrapper around a previously developed tool set for compositional verification of control flow safety properties, where program data is abstracted a way completely. We evaluate the technique on a small but realistic case study.

  • 34.
    Soleimanifard, Siavash
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Gurov, Dilian
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Huisman, Marieke
    University of Twente.
    ProMoVer: Modular Verification of Temporal Safety Properties2011In: Software Engineering and Formal Methods (SEFM) 2011, Springer , 2011, 366-381 p.Conference paper (Refereed)
    Abstract [en]

    This paper describes ProMoVer, a tool for fully automated procedure–modular verification of Java programs equipped with method–local and global assertions that specify safety properties of sequences of method invocations. Modularity at the procedure–level is a natural instantiation of the modular verification paradigm, where correctness ofglobal properties is relativized on the local properties of the methods rather than on their implementations, and is based here on the construction of maximal models for a program model that abstracts away from program data. This approach allows global properties to be verified in the presence of code evolution, multiple method implementations (as arising from software product lines), or even unknown method implementations (as in mobile code for open platforms). ProMoVer automates a typical verification scenario for a previously developed tool set for compositionalverification of control flow safety properties, and provides appropriatepre– and post–processing. Modularity is exploited by a mechanism for proof reuse that detects and minimizes the verfication tasks resulting from changes in the code and the specifications. The verification task is relatively light–weight due to support for abstraction from private methods and automatic extraction of candidate specifications from methodimplementations. We evaluate the tool on a number of applications from the smart card domain.

  • 35.
    Soleimanifard, Siavash
    et al.
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Gurov, Dilian
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Østvold, Bjarte M.
    Norwegian Computing Center, Oslo.
    Markov, Minko
    University of Sofia, Sofia.
    Model Mining and Efficient Verification of Software Product LinesManuscript (preprint) (Other academic)
  • 36. Sprenger, Christoph
    et al.
    Gurov, Dilian
    KTH, Superseded Departments, Microelectronics and Information Technology, IMIT.
    Huisman, Marieke
    Compositional verification for secure loading of smart card applets2004In: SECOND ACM AND IEEE INTERNATIONAL CONFERENCE ON FORMAL METHODS AND MODELS FOR CO-DESIGN, PROCEEDINGS, 2004, 211-222 p.Conference paper (Refereed)
    Abstract [en]

    We present an algorithmic compositional verification method for smart card applets and control flow based safety properties expressed in a modal logic with simultaneous greatest fixed points. Our method builds on a technique proposed by Grumberg and Long who use maximal models to reduce compositional verification of finite-state parallel processes to standard model checking. We adapt this technique to applets, a class of infinite-state sequential processes. This requires a refinement of the method, since for a given applet interface and behavioural formula a maximal applet does not always exist. We therefore propose a two-level approach, where local assumptions restrict the control flow structure of applets, while the global guarantee restricts the control flow behaviour of the system. We present a novel maximal model construction for our logic and then adapt it to applets. By separating the tasks of verifying global and local properties our method supports secure post-issuance loading of applets onto a smart card.

  • 37.
    Westman, Jonas
    et al.
    KTH, School of Industrial Engineering and Management (ITM), Machine Design (Dept.), Mechatronics.
    Nyberg, Mattias
    KTH, School of Industrial Engineering and Management (ITM), Machine Design (Dept.), Mechatronics.
    Gustavsson, Joakim
    KTH, School of Industrial Engineering and Management (ITM), Machine Design (Dept.), Mechatronics.
    Gurov, Dilian
    KTH, School of Computer Science and Communication (CSC), Theoretical Computer Science, TCS.
    Formal Architecture Modeling of Sequential Non-Recursive C Programs2017In: Science of Computer Programming, ISSN 0167-6423, E-ISSN 1872-7964, Vol. 146, 2-27 p.Article in journal (Refereed)
    Abstract [en]

    To manage the complexity of C programs, architecture models are used as high-level descriptions, allowing developers to understand, assess, and manage the C programs without having to understand the intricate complexity of the code implementations. However, for the architecture models to serve their purpose, they must be accurate representations of the C programs. In order to support creating accurate architecture models, the present paper presents a mapping from the domain of sequential non-recursive C programs to a domain of formal architecture models, each being a hierarchy of components with well-defined interfaces. The hierarchically organized components and their interfaces, which capture both data and function call dependencies, are shown to both enable high-level assessment and analysis of the C program and provide a foundation for organizing and expressing specifications for compositional verification.

1 - 37 of 37
CiteExportLink to result list
Permanent link
Cite
Citation style
  • apa
  • harvard1
  • ieee
  • modern-language-association-8th-edition
  • vancouver
  • Other style
More styles
Language
  • de-DE
  • en-GB
  • en-US
  • fi-FI
  • nn-NO
  • nn-NB
  • sv-SE
  • Other locale
More languages
Output format
  • html
  • text
  • asciidoc
  • rtf