본문 바로가기
HOME> 저널/프로시딩 > 저널/프로시딩 검색상세

저널/프로시딩 상세정보

권호별목차 / 소장처보기

H : 소장처정보

T : 목차정보

The journal of logical and algebraic methods in pr... 6건

  1. [해외논문]   Editorial Board   SCI SCIE


    The journal of logical and algebraic methods in programming v.96 ,pp. ii - ii , 2018 , 2352-2208 ,

    초록

    원문보기

    원문보기
    무료다운로드 유료다운로드

    회원님의 원문열람 권한에 따라 열람이 불가능 할 수 있으며 권한이 없는 경우 해당 사이트의 정책에 따라 회원가입 및 유료구매가 필요할 수 있습니다.이동하는 사이트에서의 모든 정보이용은 NDSL과 무관합니다.

    NDSL에서는 해당 원문을 복사서비스하고 있습니다. 아래의 원문복사신청 또는 장바구니담기를 통하여 원문복사서비스 이용이 가능합니다.

    이미지

    Fig. 1 이미지
  2. [해외논문]   System-level state equality detection for the formal dynamic verification of legacy distributed applications   SCI SCIE

    Guthmuller, Marion (LORIA laboratory (Université) , Corona, Gabriel (de Lorraine, CNRS, Inria Veridis), Nancy, France ) , Quinson, Martin (LORIA laboratory (Université)
    The journal of logical and algebraic methods in programming v.96 ,pp. 1 - 11 , 2018 , 2352-2208 ,

    초록

    Abstract The ever increasing complexity of distributed systems mandates to formally verify their design and implementation. Unfortunately, the common approaches and existing tools to formally establish the correctness of these systems remain hardly applicable to most legacy HPC applications, that are commonly written in Fortran or C/C++, using the MPI standard. This work addresses the problem of automatically detecting at system-level the equality of the application's state. This allows to automatically verify safety and liveness properties on legacy HPC applications. We present how this state equality detection can be achieved without any source code static analysis, but at runtime using memory introspection and classical debugging techniques. We demonstrate the effectiveness of our approach through the exhaustive verification of several programs from the MPICH3 test suite and through the partial termination analysis of some applications from the Competition on Software Verification (SV-COMP). Highlights We motivate the use of system-level state equality for dynamic verification. We present the technical locks toward state equality in legacy C/C++ Fortran code. We propose an heuristic to address these technical difficulties at runtime. We achieve an exhaustive verification of several integration tests of MPICH3. We detect the non-termination of test cases from the Competition on Software Verification (SV-COMP).

    원문보기

    원문보기
    무료다운로드 유료다운로드

    회원님의 원문열람 권한에 따라 열람이 불가능 할 수 있으며 권한이 없는 경우 해당 사이트의 정책에 따라 회원가입 및 유료구매가 필요할 수 있습니다.이동하는 사이트에서의 모든 정보이용은 NDSL과 무관합니다.

    NDSL에서는 해당 원문을 복사서비스하고 있습니다. 아래의 원문복사신청 또는 장바구니담기를 통하여 원문복사서비스 이용이 가능합니다.

    이미지

    Fig. 1 이미지
  3. [해외논문]   Labelled graph strategic rewriting for social networks   SCI SCIE

    Ferná (King's College London, UK ) , ndez, Maribel (Inria, France ) , Kirchner, Hé (University of Bordeaux, CNRS UMR5800 LaBRI, France ) , lè (University of Bordeaux, CNRS UMR5800 LaBRI, France) , ne , Pinaud, Bruno , Vallet, Jason
    The journal of logical and algebraic methods in programming v.96 ,pp. 12 - 40 , 2018 , 2352-2208 ,

    초록

    Abstract We propose an algebraic and logical approach to the study of social networks, where network components and processes are directly defined by labelled port graph strategic rewriting. Data structures attached to graph elements (nodes, ports and edges) model local and global knowledge in the network, rewrite rules express elementary and local transformations, and strategies control the global evolution of the network. We show how this approach can be used to generate random networks, simulate existing propagation and dissemination mechanisms, and design new, improved algorithms.

    원문보기

    원문보기
    무료다운로드 유료다운로드

    회원님의 원문열람 권한에 따라 열람이 불가능 할 수 있으며 권한이 없는 경우 해당 사이트의 정책에 따라 회원가입 및 유료구매가 필요할 수 있습니다.이동하는 사이트에서의 모든 정보이용은 NDSL과 무관합니다.

    NDSL에서는 해당 원문을 복사서비스하고 있습니다. 아래의 원문복사신청 또는 장바구니담기를 통하여 원문복사서비스 이용이 가능합니다.

    이미지

    Fig. 1 이미지
  4. [해외논문]   Reduction semantics in Markovian process algebra   SCI SCIE

    Bravetti, Mario
    The journal of logical and algebraic methods in programming v.96 ,pp. 41 - 64 , 2018 , 2352-2208 ,

    초록

    Abstract Markovian process algebras allow for performance analysis by automatic generation of Continuous Time Markov Chains. The inclusion of exponential distribution rate information in process algebra terms, however, causes non-trivial issues to arise in the definition of their semantics. As a consequence, technical settings previously considered do not make it possible to base Markovian semantics on directly computing reductions between communicating processes: this would require the ability to readjust processes, i.e. a commutative and associative parallel operator and a congruence relation on terms enacting such properties. Semantics in reduction style is, however, often used for complex languages, due to its simplicity and conciseness. In this paper we introduce a new technique based on stochastic binders that allows us to define Markovian semantics in the presence of such a structural congruence. As application examples, we define the reduction semantics of Markovian versions of the π -calculus, considering both the cases of Markovian durations: being additional standalone prefixes (as in Interactive Markov Chains) and being, instead, associated to standard synchronizable actions, giving them a duration (as in Stochastic π -calculus). Notably, in the latter case, we obtain a “natural” Markovian semantics for π -calculus (CCS) parallel that preserves, for the first time, its associativity. In both cases we show our technique for defining reduction semantics to be correct with respect to the standard Markovian one (in labeled style) by providing Markovian extensions of the classical π -calculus Harmony theorem.

    원문보기

    원문보기
    무료다운로드 유료다운로드

    회원님의 원문열람 권한에 따라 열람이 불가능 할 수 있으며 권한이 없는 경우 해당 사이트의 정책에 따라 회원가입 및 유료구매가 필요할 수 있습니다.이동하는 사이트에서의 모든 정보이용은 NDSL과 무관합니다.

    NDSL에서는 해당 원문을 복사서비스하고 있습니다. 아래의 원문복사신청 또는 장바구니담기를 통하여 원문복사서비스 이용이 가능합니다.

    이미지

    Fig. 1 이미지
  5. [해외논문]   Verification of finite-state machines: A distributed approach   SCI SCIE

    Gorrieri, Roberto
    The journal of logical and algebraic methods in programming v.96 ,pp. 65 - 80 , 2018 , 2352-2208 ,

    초록

    Abstract Finite-state machines, a simple class of finite Petri nets, are equipped with a truly concurrent, bisimulation-based, behavioral equivalence, called team equivalence , which conservatively extends classic bisimulation equivalence over labeled transition systems and which is checked in a distributed manner, without necessarily building a global model of the overall behavior. An associated distributed modal logic, called basic team modal logic (BTML, for short), is presented and shown to be coherent with team equivalence: two markings are team equivalent if and only if they satisfy the same BTML formulae.

    원문보기

    원문보기
    무료다운로드 유료다운로드

    회원님의 원문열람 권한에 따라 열람이 불가능 할 수 있으며 권한이 없는 경우 해당 사이트의 정책에 따라 회원가입 및 유료구매가 필요할 수 있습니다.이동하는 사이트에서의 모든 정보이용은 NDSL과 무관합니다.

    NDSL에서는 해당 원문을 복사서비스하고 있습니다. 아래의 원문복사신청 또는 장바구니담기를 통하여 원문복사서비스 이용이 가능합니다.

    이미지

    Fig. 1 이미지
  6. [해외논문]   Metalevel algorithms for variant satisfiability   SCI SCIE

    Skeirik, Stephen (Corresponding author.) , Meseguer, José
    The journal of logical and algebraic methods in programming v.96 ,pp. 81 - 110 , 2018 , 2352-2208 ,

    초록

    Abstract Variant satisfiability is a theory-generic algorithm to decide quantifier-free satisfiability in an initial algebra T Σ / E when the theory ( Σ , E ) has the finite variant property and its constructors satisfy a compactness condition. This paper: (i) gives a precise definition of several meta-level sub-algorithms needed for variant satisfiability; (ii) proves them correct; and (iii) presents a reflective implementation of variant satisfiability checking using these sub-algorithms in Maude 2.7.1.

    원문보기

    원문보기
    무료다운로드 유료다운로드

    회원님의 원문열람 권한에 따라 열람이 불가능 할 수 있으며 권한이 없는 경우 해당 사이트의 정책에 따라 회원가입 및 유료구매가 필요할 수 있습니다.이동하는 사이트에서의 모든 정보이용은 NDSL과 무관합니다.

    NDSL에서는 해당 원문을 복사서비스하고 있습니다. 아래의 원문복사신청 또는 장바구니담기를 통하여 원문복사서비스 이용이 가능합니다.

    이미지

    Fig. 1 이미지

논문관련 이미지