About: Monotonic Abstraction for Programs with Multiply-Linked Structures

Facets (new session)
Description
Metadata
Settings
- owl:sameAs
- Inference Rule:

About: Monotonic Abstraction for Programs with Multiply-Linked Structures Goto Sponge NotDistinct Permalink

An Entity of Type : http://linked.opendata.cz/ontology/domain/vavai/Vysledek, within Data Space : linked.opendata.cz associated with source document(s)

Attributes	Values
rdf:type	skos:Concept http://linked.opendata.cz/ontology/domain/vavai/Vysledek
rdfs:seeAlso	http://www.worldscientific.com/doi/abs/10.1142/S0129054113400078
Description	We investigate the use of monotonic abstraction and backward reachability analysis as means of performing shape analysis on programs with multiply pointed structures. By encoding the heap as a vertex- and edge-labeled graph, we can model the low level behaviour exhibited by programs written in the C programming language. Using the notion of signatures, which are predicates that define sets of heaps, we can check properties such as absence of null pointer dereference and shape invariants. We report on the results from running a prototype based on the method on several programs such as insertion into and merging of doubly-linked lists. We investigate the use of monotonic abstraction and backward reachability analysis as means of performing shape analysis on programs with multiply pointed structures. By encoding the heap as a vertex- and edge-labeled graph, we can model the low level behaviour exhibited by programs written in the C programming language. Using the notion of signatures, which are predicates that define sets of heaps, we can check properties such as absence of null pointer dereference and shape invariants. We report on the results from running a prototype based on the method on several programs such as insertion into and merging of doubly-linked lists. (en)
Title	Monotonic Abstraction for Programs with Multiply-Linked Structures Monotonic Abstraction for Programs with Multiply-Linked Structures (en)
skos:prefLabel	Monotonic Abstraction for Programs with Multiply-Linked Structures Monotonic Abstraction for Programs with Multiply-Linked Structures (en)
skos:notation	RIV/00216305:26230/13:PU106375!RIV14-GA0-26230___
http://linked.open...avai/predkladatel	Fakulta informačních technologií
http://linked.open...avai/riv/aktivita	P S Z
http://linked.open...avai/riv/aktivity	P(ED1.1.00/02.0070), P(GAP103/10/0306), P(OC10009), S, Z(MSM0021630528)
http://linked.open...iv/cisloPeriodika	2
http://linked.open...vai/riv/dodaniDat	2014
http://linked.open...aciTvurceVysledku	Vojnar, Tomáš
http://linked.open.../riv/druhVysledku	J - Článek v odborném periodiku
http://linked.open...iv/duvernostUdaju	S - Úplné a pravdivé údaje nepodléhající ochraně podle zvláštních právních předpisů
http://linked.open...titaPredkladatele	Vysoké učení technické v Brně / Fakulta informačních technologií
http://linked.open...dnocenehoVysledku	89498
http://linked.open...ai/riv/idVysledku	RIV/00216305:26230/13:PU106375
http://linked.open...riv/jazykVysledku	eng - angličtina
http://linked.open.../riv/klicovaSlova	formal verification, program analysis, upward closed sets, monotonic abstraction, dynamic memory, pointers, dynamic linked data structures, multiple selectors, doubly-linked lists, trees, null pointer dereference, dangling pointers, memory leakage (en)
http://linked.open.../riv/klicoveSlovo	dynamic linked data structures dangling pointers doubly-linked lists dynamic memory memory leakage monotonic abstraction multiple selectors null pointer dereference pointers program analysis upward closed sets trees formal verification
http://linked.open...odStatuVydavatele	SG - Singapurská republika
http://linked.open...ontrolniKodProRIV	[0BA0B6959284]
http://linked.open...i/riv/nazevZdroje	International Journal of Foundations of Computer Science
http://linked.open...in/vavai/riv/obor	IN
http://linked.open...ichTvurcuVysledku	1 (xsd:int)
http://linked.open...cetTvurcuVysledku	3 (xsd:int)
http://linked.open...vavai/riv/projekt	IT4Innovations Centre of Excellence Static and Dynamic Verification of Programs with Advanced Features of Concurrency and Unboundedness Dealing with Complex Data Structures and Concurrency within the Rich Model Toolkit
http://linked.open...UplatneniVysledku	2013
http://linked.open...v/svazekPeriodika	24
http://linked.open...iv/tvurceVysledku	Abdulla, Parosh Vojnar, Tomáš Cederberg, Jonathan
http://linked.open...n/vavai/riv/zamer	Výzkum informačních technologií z hlediska bezpečnosti
issn	0129-0541
number of pages	24 (xsd:int)
http://bibframe.org/vocab/doi	10.1142/S0129054113400078
http://localhost/t...ganizacniJednotka	26230

Faceted Search & Find service v1.16.118 as of Jun 21 2024

Alternative Linked Data Documents: ODE Content Formats:

RDF

ODATA

Microdata

About

OpenLink Virtuoso version 07.20.3240 as of Jun 21 2024, on Linux (x86_64-pc-linux-gnu), Single-Server Edition (126 GB total memory, 58 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software