LIVIVO - The Search Portal for Life Sciences

zur deutschen Oberfläche wechseln
Advanced search

Search results

Result 1 - 10 of total 494

Search options

  1. Book ; Online: Exact Separation Logic (Extended Version)

    Maksimović, Petar / Cronjäger, Caroline / Lööw, Andreas / Sutherland, Julian / Gardner, Philippa

    2022  

    Abstract: Over-approximating (OX) program logics, such as separation logic (SL), are used for verifying properties of heap-manipulating programs: all terminating behaviour is characterised, but established results and errors need not be reachable. OX function ... ...

    Abstract Over-approximating (OX) program logics, such as separation logic (SL), are used for verifying properties of heap-manipulating programs: all terminating behaviour is characterised, but established results and errors need not be reachable. OX function specifications are thus incompatible with true bug-finding supported by symbolic execution tools such as Pulse and Pulse-X. In contrast, under-approximating (UX) program logics, such as incorrectness separation logic, are used to find true results and bugs: established results and errors are reachable, but there is no mechanism for understanding if all terminating behaviour has been characterised. We introduce exact separation logic (ESL), which provides fully-verified function specifications compatible with both OX verification and UX true bug-funding: all terminating behaviour is characterised, and all established results and errors are reachable. We prove soundness for ESL with mutually recursive functions, demonstrating, for the first time, function compositionality for a UX logic. We show that UX program logics require subtle definitions of internal and external function specifications compared with the familiar definitions of OX logics. We investigate the expressivity of ESL and, for the first time, explore the role of abstraction in UX reasoning by verifying abstract ESL specifications of various data-structure algorithms. In doing so, we highlight the difference between abstraction (hiding information) and over-approximation (losing information). Our findings demonstrate that, expectedly, abstraction cannot be used as freely in UX logics as in OX logics, but also that it should be feasible to use ESL to provide tractable function specifications for self-contained, critical code, which would then be used for both verification and true bug-finding.
    Keywords Computer Science - Logic in Computer Science ; Computer Science - Programming Languages
    Subject code 004
    Publishing date 2022-08-15
    Publishing country us
    Document type Book ; Online
    Database BASE - Bielefeld Academic Search Engine (life sciences selection)

    Full text online

    More links

    Kategorien

    Inter-library loan at ZB MED

    Your chosen title can be delivered directly to ZB MED Cologne location if you are registered as a user at ZB MED Cologne.

  2. Book ; Online: Gillian

    Maksimović, Petar / Santos, José Fragoso / Ayoun, Sacha-Élie / Gardner, Philippa

    A Multi-Language Platform for Unified Symbolic Analysis

    2021  

    Abstract: This is an evolving document describing the meta-theory, the implementation, and the instantiations of Gillian, a multi-language symbolic analysis platform. ...

    Abstract This is an evolving document describing the meta-theory, the implementation, and the instantiations of Gillian, a multi-language symbolic analysis platform.
    Keywords Computer Science - Programming Languages ; Computer Science - Logic in Computer Science
    Publishing date 2021-05-31
    Publishing country us
    Document type Book ; Online
    Database BASE - Bielefeld Academic Search Engine (life sciences selection)

    Full text online

    More links

    Kategorien

    Inter-library loan at ZB MED

    Your chosen title can be delivered directly to ZB MED Cologne location if you are registered as a user at ZB MED Cologne.

  3. Book ; Online: Gillian

    Santos, José Fragoso / Maksimović, Petar / Ayoun, Sacha-Élie / Gardner, Philippa

    Compositional Symbolic Execution for All

    2020  

    Abstract: We present Gillian, a language-independent framework for the development of compositional symbolic analysis tools. Gillian supports three flavours of analysis: whole-program symbolic testing, full verification, and bi-abduction. It comes with fully ... ...

    Abstract We present Gillian, a language-independent framework for the development of compositional symbolic analysis tools. Gillian supports three flavours of analysis: whole-program symbolic testing, full verification, and bi-abduction. It comes with fully parametric meta-theoretical results and a modular implementation, designed to minimise the instantiation effort required of the user. We evaluate Gillian by instantiating it to JavaScript and C, and perform its analyses on a set of data-structure libraries, obtaining results that indicate that Gillian is robust enough to reason about real-world programming languages.
    Keywords Computer Science - Programming Languages ; Computer Science - Logic in Computer Science
    Publishing date 2020-01-14
    Publishing country us
    Document type Book ; Online
    Database BASE - Bielefeld Academic Search Engine (life sciences selection)

    Full text online

    More links

    Kategorien

    Inter-library loan at ZB MED

    Your chosen title can be delivered directly to ZB MED Cologne location if you are registered as a user at ZB MED Cologne.

  4. Book ; Online: $\mathsf{LLF}_{\cal P}$

    Honsell, Furio / Liquori, Luigi / Maksimovic, Petar / Scagnetto, Ivan

    a logical framework for modeling external evidence, side conditions, and proof irrelevance using monads

    2017  

    Abstract: We extend the constructive dependent type theory of the Logical Framework $\mathsf{LF}$ with monadic, dependent type constructors indexed with predicates over judgements, called Locks. These monads capture various possible proof attitudes in establishing ...

    Abstract We extend the constructive dependent type theory of the Logical Framework $\mathsf{LF}$ with monadic, dependent type constructors indexed with predicates over judgements, called Locks. These monads capture various possible proof attitudes in establishing the judgment of the object logic encoded by an $\mathsf{LF}$ type. Standard examples are factoring-out the verification of a constraint or delegating it to an external oracle, or supplying some non-apodictic epistemic evidence, or simply discarding the proof witness of a precondition deeming it irrelevant. This new framework, called Lax Logical Framework, $\mathsf{LLF}_{\cal P}$, is a conservative extension of $\mathsf{LF}$, and hence it is the appropriate metalanguage for dealing formally with side-conditions in rules or external evidence in logical systems. $\mathsf{LLF}_{\cal P}$ arises once the monadic nature of the lock type-constructor, ${\cal L}^{\cal P}_{M,\sigma}[\cdot]$, introduced by the authors in a series of papers, together with Marina Lenisa, is fully exploited. The nature of the lock monads permits to utilize the very Lock destructor, ${\cal U}^{\cal P}_{M,\sigma}[\cdot]$, in place of Moggi's monadic $let_T$, thus simplifying the equational theory. The rules for ${\cal U}^{\cal P}_{M,\sigma}[\cdot]$ permit also the removal of the monad once the constraint is satisfied. We derive the meta-theory of $\mathsf{LLF}_{\cal P}$ by a novel indirect method based on the encoding of $\mathsf{LLF}_{\cal P}$ in $\mathsf{LF}$. We discuss encodings in $\mathsf{LLF}_{\cal P}$ of call-by-value $\lambda$-calculi, Hoare's Logic, and Fitch-Prawitz Naive Set Theory.

    Comment: Accepted for publication in LMCS
    Keywords Computer Science - Logic in Computer Science ; F.4.1
    Subject code 160
    Publishing date 2017-02-23
    Publishing country us
    Document type Book ; Online
    Database BASE - Bielefeld Academic Search Engine (life sciences selection)

    Full text online

    More links

    Kategorien

    Inter-library loan at ZB MED

    Your chosen title can be delivered directly to ZB MED Cologne location if you are registered as a user at ZB MED Cologne.

  5. Book ; Online: A Program Logic for First-Order Encapsulated WebAssembly

    Watt, Conrad / Maksimović, Petar / Krishnaswami, Neelakantan R. / Gardner, Philippa

    2018  

    Abstract: We introduce Wasm Logic, a sound program logic for first-order, encapsulated WebAssembly. We design a novel assertion syntax, tailored to WebAssembly's stack-based semantics and the strong guarantees given by WebAssembly's type system, and show how to ... ...

    Abstract We introduce Wasm Logic, a sound program logic for first-order, encapsulated WebAssembly. We design a novel assertion syntax, tailored to WebAssembly's stack-based semantics and the strong guarantees given by WebAssembly's type system, and show how to adapt the standard separation logic triple and proof rules in a principled way to capture WebAssembly's uncommon structured control flow. Using Wasm Logic, we specify and verify a simple WebAssembly B-tree library, giving abstract specifications independent of the underlying implementation. We mechanise Wasm Logic and its soundness proof in full in Isabelle/HOL. As part of the soundness proof, we formalise and fully mechanise a novel, big-step semantics of WebAssembly, which we prove equivalent, up to transitive closure, to the original WebAssembly small-step semantics. Wasm Logic is the first program logic for WebAssembly, and represents a first step towards the creation of static analysis tools for WebAssembly.

    Comment: 50 pages, 17 figures
    Keywords Computer Science - Programming Languages
    Subject code 005
    Publishing date 2018-11-08
    Publishing country us
    Document type Book ; Online
    Database BASE - Bielefeld Academic Search Engine (life sciences selection)

    Full text online

    More links

    Kategorien

    Inter-library loan at ZB MED

    Your chosen title can be delivered directly to ZB MED Cologne location if you are registered as a user at ZB MED Cologne.

  6. Article: Stress-incontinentie bij de vrouw; resultaten van de operatieve behandeling volgens Stamey-Pereyra.

    Maksimovic, P / Schröder, F H / Kurth, K H

    Nederlands tijdschrift voor geneeskunde

    1985  Volume 129, Issue 20, Page(s) 951–954

    Title translation Stress incontinence in women; results of the Stamey-Pereyra surgical treatment method.
    MeSH term(s) Adult ; Aged ; Female ; Follow-Up Studies ; Humans ; Methods ; Middle Aged ; Postoperative Complications/etiology ; Urinary Incontinence, Stress/surgery ; Urinary Tract Infections/etiology
    Language Dutch
    Publishing date 1985-05-18
    Publishing country Netherlands
    Document type English Abstract ; Journal Article
    ZDB-ID 82073-8
    ISSN 1876-8784 ; 0028-2162
    ISSN (online) 1876-8784
    ISSN 0028-2162
    Database MEDical Literature Analysis and Retrieval System OnLINE

    More links

    Kategorien

    In stock of ZB MED Cologne/Königswinter

    Ua VI Zs.18: Show issues Location:
    Je nach Verfügbarkeit (siehe Angabe bei Bestand)
    bis Jg. 2021: Bestellungen von Artikeln über das Online-Bestellformular
    ab Jg. 2022: Lesesaal (EG)

    Order via subito

    This service is chargeable due to the Delivery terms set by subito. Orders including an article and supplementary material will be classified as separate orders. In these cases, fees will be demanded for each order.

  7. Article: Open science grid study of the coupling between conformation and water content in the interior of a protein.

    Damjanović, Ana / Miller, Benjamin T / Wenaus, Torre J / Maksimović, Petar / García-Moreno E, Bertrand / Brooks, Bernard R

    Journal of chemical information and modeling

    2008  Volume 48, Issue 10, Page(s) 2021–2029

    Abstract: Computational grids are a promising resource for modeling complex biochemical processes such as protein folding, penetration of gases or water into proteins, or protein structural rearrangements coupled to ligand binding. We have enabled the molecular ... ...

    Abstract Computational grids are a promising resource for modeling complex biochemical processes such as protein folding, penetration of gases or water into proteins, or protein structural rearrangements coupled to ligand binding. We have enabled the molecular dynamics program CHARMM to run on the Open Science Grid. The implementation is general, flexible, easily modifiable for use with other molecular dynamics programs and other grids and automated in terms of job submission, monitoring, and resubmission. The usefulness of grid computing was demonstrated through the study of hydration of the Glu-66 side chain in the interior of protein staphylococcal nuclease. Multiple simulations started with and without two internal water molecules shown crystallographically to be associated with the side chain of Glu-66 yielded two distinct populations of rotameric states of Glu-66 that differed by as much as 20%. This illustrates how internal water molecules can bias protein conformations. Furthermore, there appeared to be a temporal correlation between dehydration of the side chain and conformational transitions of Glu-66. This example demonstrated how difficult it is to get convergence even in the relatively simple case of a side chain oscillating between two conformations. With grid computing, we also benchmarked the self-guided Langevin dynamics method against the Langevin dynamics method traditionally used for temperature control in molecular dynamics simulations and showed that the two methods yield comparable results.
    MeSH term(s) Computer Simulation ; Gases/chemistry ; Glutamic Acid/chemistry ; Ligands ; Protein Binding ; Protein Conformation ; Protein Folding ; Proteins/chemistry ; Water/chemistry
    Chemical Substances Gases ; Ligands ; Proteins ; Water (059QF0KO0R) ; Glutamic Acid (3KX376GY7L)
    Language English
    Publishing date 2008-10
    Publishing country United States
    Document type Journal Article ; Research Support, N.I.H., Extramural ; Research Support, N.I.H., Intramural ; Research Support, Non-U.S. Gov't ; Research Support, U.S. Gov't, Non-P.H.S.
    ZDB-ID 190019-5
    ISSN 1549-9596 ; 0095-2338
    ISSN 1549-9596 ; 0095-2338
    DOI 10.1021/ci800263c
    Database MEDical Literature Analysis and Retrieval System OnLINE

    More links

    Kategorien

    In stock of ZB MED Cologne/Königswinter

    Zs.A 1230: Show issues Location:
    Je nach Verfügbarkeit (siehe Angabe bei Bestand)
    bis Jg. 1994: Bestellungen von Artikeln über das Online-Bestellformular
    Jg. 1995 - 2021: Lesesall (1.OG)
    ab Jg. 2022: Lesesaal (EG)

    Order via subito

    This service is chargeable due to the Delivery terms set by subito. Orders including an article and supplementary material will be classified as separate orders. In these cases, fees will be demanded for each order.

  8. Article: Intracavernous injection during diagnostic screening for erectile dysfunction; five-year experience with over 600 patients.

    Slob, A K / Verhulst, A C M / Gijs, L / Maksimovic, P A / van der Werff ten Bosch, J J

    Journal of sex & marital therapy

    2002  Volume 28, Issue 1, Page(s) 61–70

    Abstract: Psychophysiological diagnostic screening (PDS) was carried out on just over 1000 consecutive patients with erectile dysfunction (ED) during 1995 through 1999. Roughly one-third did not require an intracavernous injection (ICI) because of optimal penile ... ...

    Abstract Psychophysiological diagnostic screening (PDS) was carried out on just over 1000 consecutive patients with erectile dysfunction (ED) during 1995 through 1999. Roughly one-third did not require an intracavernous injection (ICI) because of optimal penile response during visual and tactile penile sexual stimulation. The present article deals with those other patients (n = 609) who required an ICI and completed a 24-hour-postinvestigation questionnaire (PIQ). The two ICI preparations used, prostaglandin and papaverine + fentolamine, were virtually equally effective in the doses applied, with very low and similar percentages of unwanted side effects, for example, prolonged erection. Somatic ED patients displayed the lowest penile responses to ICI, whereas psychogenic ED patients had the highest penile responses. ED patients who also suffered from premature ejaculation (PE) ejaculated significantly more readily during PDS that those without PE. An ICI following an ejaculation/orgasm could lead to an erection presumably sufficient for intromission, which indicates ICI as a therapeutic option for rapid ejaculators. Our elaborate and lengthy PDS procedure, particularly the use of penile vibration as an addition to the visual sexual stimulation, obviates the diagnostic use of the PIQ.
    MeSH term(s) Adjuvants, Immunologic/administration & dosage ; Adjuvants, Immunologic/therapeutic use ; Adolescent ; Adult ; Aged ; Dehydroepiandrosterone/administration & dosage ; Dehydroepiandrosterone/therapeutic use ; Drug Administration Routes ; Erectile Dysfunction/drug therapy ; Erectile Dysfunction/epidemiology ; Humans ; Injections ; Male ; Mass Screening ; Middle Aged ; Surveys and Questionnaires
    Chemical Substances Adjuvants, Immunologic ; Dehydroepiandrosterone (459AG36T1B)
    Language English
    Publishing date 2002-04-02
    Publishing country England
    Document type Journal Article
    ZDB-ID 752393-2
    ISSN 0092-623X
    ISSN 0092-623X
    DOI 10.1080/009262302317251025
    Database MEDical Literature Analysis and Retrieval System OnLINE

    More links

    Kategorien

    In stock of ZB MED Cologne/Königswinter

    Zs.A 1317: Show issues Location:
    Je nach Verfügbarkeit (siehe Angabe bei Bestand)
    bis Jg. 1994: Bestellungen von Artikeln über das Online-Bestellformular
    Jg. 1995 - 2021: Lesesall (1.OG)
    ab Jg. 2022: Lesesaal (EG)

    Order via subito

    This service is chargeable due to the Delivery terms set by subito. Orders including an article and supplementary material will be classified as separate orders. In these cases, fees will be demanded for each order.

  9. Article: Vasectomy and cholesterol.

    Verheugt, F W / Tijssen, J G / Boerma, G J / Maksimovic, P / Miranda, S I

    The New England journal of medicine

    1981  Volume 305, Issue 8, Page(s) 462

    MeSH term(s) Adult ; Cholesterol/blood ; Humans ; Male ; Prospective Studies ; Vasectomy/adverse effects
    Chemical Substances Cholesterol (97C5T2UQ7J)
    Language English
    Publishing date 1981-08-20
    Publishing country United States
    Document type Letter
    ZDB-ID 207154-x
    ISSN 1533-4406 ; 0028-4793
    ISSN (online) 1533-4406
    ISSN 0028-4793
    Database MEDical Literature Analysis and Retrieval System OnLINE

    More links

    Kategorien

    In stock of ZB MED Cologne/Königswinter

    Ua VI Zs.34: Show issues Location:
    Je nach Verfügbarkeit (siehe Angabe bei Bestand)
    bis Jg. 2021: Bestellungen von Artikeln über das Online-Bestellformular
    ab Jg. 2022: Lesesaal (EG)

    Order via subito

    This service is chargeable due to the Delivery terms set by subito. Orders including an article and supplementary material will be classified as separate orders. In these cases, fees will be demanded for each order.

  10. Article: Influence of plowing-in of corn-stalks on some soil properties and corn yield with and without irrigation

    Jovanovic, R / Maksimovic, P / Franic, I

    1972 (Transl. 1973), 25 (89)

    1972  

    Keywords plants ; plant cultural practices ; field crops ; crop production ; agronomy
    Language English
    Size p. 43-50.
    Document type Article
    Note Translated from Arhiv za Poljoprivredne Nauke, 25(89):39-48. 1972. (21.5 Y9)
    Database NAL-Catalogue (AGRICOLA)

    Kategorien

    Inter-library loan at ZB MED

    Your chosen title can be delivered directly to ZB MED Cologne location if you are registered as a user at ZB MED Cologne.

To top