Pretraga

Pretražite po imenu i prezimenu autora, mentora, urednika, prevoditelja

Napredna pretraga

Pregled bibliografske jedinice broj: 399647

Separation Logic Verification of C Programs with an SMT Solver

Botinčan, Matko; Parkinson, Matthew; Schulte, Wolfram
Separation Logic Verification of C Programs with an SMT Solver // Proceedings of the 4th International Workshop on Systems Software Verification (SSV 09) / Huuck, Ralf ; Klein, Gerwin ; Schlich, Bastian (ur.).
Aachen, Njemačka: Elsevier, 2009. (predavanje, međunarodna recenzija, cjeloviti rad (in extenso), znanstveni)

CROSBI ID: 399647 Za ispravke kontaktirajte CROSBI podršku putem web obrasca

Naslov
Separation Logic Verification of C Programs with an SMT Solver

Autori
Botinčan, Matko ; Parkinson, Matthew ; Schulte, Wolfram

Vrsta, podvrsta i kategorija rada
Radovi u zbornicima skupova, cjeloviti rad (in extenso), znanstveni

Izvornik
Proceedings of the 4th International Workshop on Systems Software Verification (SSV 09) / Huuck, Ralf ; Klein, Gerwin ; Schlich, Bastian - : Elsevier, 2009

Skup
4th International Workshop on Systems Software Verification (SSV 09)

Mjesto i datum
Aachen, Njemačka, 22.06.2009. - 24.06.2009

Vrsta sudjelovanja
Predavanje

Vrsta recenzije
Međunarodna recenzija

Ključne riječi
Separation logic; automated verification; automated theorem proving; C programming language

Sažetak
This paper presents a methodology for automated modular verification of C programs against specifications written in separation logic. The distinguishing features of the approach are representation of the C memory model in separation logic by means of rewrite rules suitable for automation and the careful integration of an SMT solver behind the separation logic prover to guide the proof search.

Izvorni jezik
Engleski

Znanstvena područja
Matematika, Računarstvo



POVEZANOST RADA

Projekti:
037-0362980-2774 - Distribuirani algoritmi za pronalaženje optimalnih putova u grafovima (Manger, Robert, MZOS ) ( CroRIS)

Ustanove:
Prirodoslovno-matematički fakultet, Matematički odjel, Zagreb

Profili:

Avatar Url Matko Botinčan (autor)

Poveznice na cjeloviti tekst rada:

Pristup cjelovitom tekstu rada

Citiraj ovu publikaciju:

Botinčan, Matko; Parkinson, Matthew; Schulte, Wolfram
Separation Logic Verification of C Programs with an SMT Solver // Proceedings of the 4th International Workshop on Systems Software Verification (SSV 09) / Huuck, Ralf ; Klein, Gerwin ; Schlich, Bastian (ur.).
Aachen, Njemačka: Elsevier, 2009. (predavanje, međunarodna recenzija, cjeloviti rad (in extenso), znanstveni)
Botinčan, M., Parkinson, M. & Schulte, W. (2009) Separation Logic Verification of C Programs with an SMT Solver. U: Huuck, R., Klein, G. & Schlich, B. (ur.)Proceedings of the 4th International Workshop on Systems Software Verification (SSV 09).
@article{article, author = {Botin\v{c}an, Matko and Parkinson, Matthew and Schulte, Wolfram}, year = {2009}, keywords = {Separation logic, automated verification, automated theorem proving, C programming language}, title = {Separation Logic Verification of C Programs with an SMT Solver}, keyword = {Separation logic, automated verification, automated theorem proving, C programming language}, publisher = {Elsevier}, publisherplace = {Aachen, Njema\v{c}ka} }
@article{article, author = {Botin\v{c}an, Matko and Parkinson, Matthew and Schulte, Wolfram}, year = {2009}, keywords = {Separation logic, automated verification, automated theorem proving, C programming language}, title = {Separation Logic Verification of C Programs with an SMT Solver}, keyword = {Separation logic, automated verification, automated theorem proving, C programming language}, publisher = {Elsevier}, publisherplace = {Aachen, Njema\v{c}ka} }

Časopis indeksira:


  • Web of Science Core Collection (WoSCC)
    • Emerging Sources Citation Index (ESCI)
  • Scopus

Podijeli:





Contrast
Increase Font
Decrease Font
Dyslexic Font
CROSBI koristi kolačiće (cookies) kako bi poboljšao funkcionalnost stranice.