Automatic Parallelization and Optimization of Programs by Proof Rewriting

Autor: Hurlin, C., Palsberg, J., Su, Z.
Přispěvatelé: Environments for Verification and Security of Software (EVEREST), Inria Sophia Antipolis - Méditerranée (CRISAM), Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Formal Methods and Tools (FMT group), University of Twente [Netherlands], IST-FET-2005-015905 Mobius project, Palsberg, Jens and Su, Zhendong, ANR-06-SETI-0010,PARSEC,PARallélisme et SECurité(2006), University of Twente, IST-FET-2005-015905 Mobius project et ANR-06-SETIN-010 ParSec project, INRIA
Jazyk: angličtina
Rok vydání: 2009
Předmět:
Theoretical computer science
Computer science
Separation Logic
METIS-263832
ACM: D.: Software/D.2: SOFTWARE ENGINEERING/D.2.4: Software/Program Verification
EWI-15321
02 engineering and technology
Separation logic
Symbolic execution
computer.software_genre
[INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL]
Proof tree
ACM: D.: Software/D.1: PROGRAMMING TECHNIQUES/D.1.3: Concurrent Programming
0202 electrical engineering
electronic engineering
information engineering
Automatic Parallelization
Programming language
020207 software engineering
ACM: D.: Software/D.1: PROGRAMMING TECHNIQUES/D.1.3: Concurrent Programming/D.1.3.1: Parallel programming
ACM: F.: Theory of Computation/F.3: LOGICS AND MEANINGS OF PROGRAMS/F.3.1: Specifying and Verifying and Reasoning about Programs
Proof rule
Automatic parallelization
TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES
TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS
Computer Science::Programming Languages
IR-67469
020201 artificial intelligence & image processing
Rewriting
computer
Proof-Preserving Optimizations
Zdroj: Static Analysis Symposium
Static Analysis Symposium, Aug 2009, Los Angeles, United States. pp.52-68
[Research Report] RR-6806, INRIA. 2009
Static Analysis ISBN: 9783642032363
SAS
The 16th International Static Analysis Symposium, 52-68
STARTPAGE=52;ENDPAGE=68;TITLE=The 16th International Static Analysis Symposium
Popis: International audience; We show how, given a program and its separation logic proof, one can parallelize and optimize this program and transform its proof simultaneously to obtain a proven parallelized and optimized program. To achieve this goal, we present new proof rules for generating proof trees and a rewrite system on proof trees.
Databáze: OpenAIRE
Externí odkaz: