InforLorV4, PascalFrancis, Corpus, bibRecord, 000B97

An experiment in parallelizing an application using formal methods: Computer aided parallelization

Identifieur interne : 000B97 ( PascalFrancis/Corpus ); précédent : 000B96; suivant : 000B98

An experiment in parallelizing an application using formal methods: Computer aided parallelization

Auteurs : R. Couturier ; D. Mery

Source :

Lecture notes in computer science [ 0302-9743 ] ; 1998.

RBID : Pascal:98-0358260

Descripteurs français

Pascal (Inist)
- Conception système, Système informatique, Système parallèle, Simulation système, Vérification formelle.

English descriptors

KwdEn :
- Computer system, Formal verification, Parallel system, System design, System simulation.

Abstract

Scientists and engineers have successfully developed much useful sequential code using classical programming languages, such as Fortran, and highly performant computers can help them to model problems whilst improving their results of simulation. However, great skill and care are required to design correct parallel code from sequential code. We focus our work on 3 aspects of producing correct parallel code from sequential code. First, we use a theorem prover, namely PVS, as a practical tool for asserting proof obligations and for stating programs and properties. Secondly, we build an abstraction from some sequential code in order to derive a postcondition. Finally, we characterize the "glueing condition" that will ensure the correctness of the final parallel code. Our method does not need any new notation but reuses proof theoretical notations together with the composition of postconditions with respect to the glueing condition.

Notice en format standard (ISO 2709)

Pour connaître la documentation sur le format Inist Standard.

A01	`01`	`1`		`@0 0302-9743`
A05				`@2 1427`
A08	`01`	`1`	`ENG`	`@1 An experiment in parallelizing an application using formal methods: Computer aided parallelization`
A09	`01`	`1`	`ENG`	`@1 CAV '98 : computer aided verification : Vancouver BC, 28 June - 2 July 1998`
A11	`01`	`1`		`@1 COUTURIER (R.)`
A11	`02`	`1`		`@1 MERY (D.)`
A12	`01`	`1`		`@1 HU (Alan J.) @9 ed.`
A12	`02`	`1`		`@1 VARDI (Moshe Y.) @9 ed.`
A14	`01`			`@1 UMR n°7503 LORIA CNRS, Université Henri Poincaré, BP 239 @2 54506 Vandœuvre-lès-Nancy @3 FRA @Z 1 aut. @Z 2 aut.`
A20				`@1 345-356`
A21				`@1 1998`
A23	`01`			`@0 ENG`
A26	`01`			`@0 3-540-64608-6`
A43	`01`			`@1 INIST @2 16343 @5 354000076380680320`
A44				`@0 0000 @1 © 1998 INIST-CNRS. All rights reserved.`
A45				`@0 15 ref.`
A47	`01`	`1`		`@0 98-0358260`
A60				`@1 P @2 C`
A61				`@0 A`
A64		`1`		`@0 Lecture notes in computer science`
A66	`01`			`@0 DEU`
A66	`02`			`@0 USA`
C01	`01`		`ENG`	@0 Scientists and engineers have successfully developed much useful sequential code using classical programming languages, such as Fortran, and highly performant computers can help them to model problems whilst improving their results of simulation. However, great skill and care are required to design correct parallel code from sequential code. We focus our work on 3 aspects of producing correct parallel code from sequential code. First, we use a theorem prover, namely PVS, as a practical tool for asserting proof obligations and for stating programs and properties. Secondly, we build an abstraction from some sequential code in order to derive a postcondition. Finally, we characterize the "glueing condition" that will ensure the correctness of the final parallel code. Our method does not need any new notation but reuses proof theoretical notations together with the composition of postconditions with respect to the glueing condition.
C02	`01`	`X`		`@0 001D02B04`
C03	`01`	`X`	`FRE`	`@0 Conception système @5 01`
C03	`01`	`X`	`ENG`	`@0 System design @5 01`
C03	`01`	`X`	`SPA`	`@0 Concepción sistema @5 01`
C03	`02`	`X`	`FRE`	`@0 Système informatique @5 02`
C03	`02`	`X`	`ENG`	`@0 Computer system @5 02`
C03	`02`	`X`	`SPA`	`@0 Sistema informático @5 02`
C03	`03`	`X`	`FRE`	`@0 Système parallèle @5 03`
C03	`03`	`X`	`ENG`	`@0 Parallel system @5 03`
C03	`03`	`X`	`SPA`	`@0 Sistema paralelo @5 03`
C03	`04`	`X`	`FRE`	`@0 Simulation système @5 04`
C03	`04`	`X`	`ENG`	`@0 System simulation @5 04`
C03	`04`	`X`	`SPA`	`@0 Simulación sistema @5 04`
C03	`05`	`3`	`FRE`	`@0 Vérification formelle @5 05`
C03	`05`	`3`	`ENG`	`@0 Formal verification @5 05`
N21				`@1 243`

A30	`01`	`1`	`ENG`	`@1 International conference on computer aided verification @2 10 @3 Vancouver BC CAN @4 1998-06-28`

Format Inist (serveur)

NO :	PASCAL 98-0358260 INIST
ET :	An experiment in parallelizing an application using formal methods: Computer aided parallelization
AU :	COUTURIER (R.); MERY (D.); HU (Alan J.); VARDI (Moshe Y.)
AF :	UMR n°7503 LORIA CNRS, Université Henri Poincaré, BP 239/54506 Vandœuvre-lès-Nancy/France (1 aut., 2 aut.)
DT :	Publication en série; Congrès; Niveau analytique
SO :	Lecture notes in computer science; ISSN 0302-9743; Allemagne; Da. 1998; Vol. 1427; Pp. 345-356; Bibl. 15 ref.
LA :	Anglais
EA :	Scientists and engineers have successfully developed much useful sequential code using classical programming languages, such as Fortran, and highly performant computers can help them to model problems whilst improving their results of simulation. However, great skill and care are required to design correct parallel code from sequential code. We focus our work on 3 aspects of producing correct parallel code from sequential code. First, we use a theorem prover, namely PVS, as a practical tool for asserting proof obligations and for stating programs and properties. Secondly, we build an abstraction from some sequential code in order to derive a postcondition. Finally, we characterize the "glueing condition" that will ensure the correctness of the final parallel code. Our method does not need any new notation but reuses proof theoretical notations together with the composition of postconditions with respect to the glueing condition.
CC :	001D02B04
FD :	Conception système; Système informatique; Système parallèle; Simulation système; Vérification formelle
ED :	System design; Computer system; Parallel system; System simulation; Formal verification
SD :	Concepción sistema; Sistema informático; Sistema paralelo; Simulación sistema
LO :	INIST-16343.354000076380680320
ID :	98-0358260

Links to Exploration step

Pascal:98-0358260

Le document en format XML

<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">An experiment in parallelizing an application using formal methods: Computer aided parallelization</title>
<author><name sortKey="Couturier, R" sort="Couturier, R" uniqKey="Couturier R" first="R." last="Couturier">R. Couturier</name>
<affiliation><inist:fA14 i1="01"><s1>UMR n°7503 LORIA CNRS, Université Henri Poincaré, BP 239</s1>
<s2>54506 Vandœuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Mery, D" sort="Mery, D" uniqKey="Mery D" first="D." last="Mery">D. Mery</name>
<affiliation><inist:fA14 i1="01"><s1>UMR n°7503 LORIA CNRS, Université Henri Poincaré, BP 239</s1>
<s2>54506 Vandœuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">INIST</idno>
<idno type="inist">98-0358260</idno>
<date when="1998">1998</date>
<idno type="stanalyst">PASCAL 98-0358260 INIST</idno>
<idno type="RBID">Pascal:98-0358260</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000B97</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">An experiment in parallelizing an application using formal methods: Computer aided parallelization</title>
<author><name sortKey="Couturier, R" sort="Couturier, R" uniqKey="Couturier R" first="R." last="Couturier">R. Couturier</name>
<affiliation><inist:fA14 i1="01"><s1>UMR n°7503 LORIA CNRS, Université Henri Poincaré, BP 239</s1>
<s2>54506 Vandœuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
<author><name sortKey="Mery, D" sort="Mery, D" uniqKey="Mery D" first="D." last="Mery">D. Mery</name>
<affiliation><inist:fA14 i1="01"><s1>UMR n°7503 LORIA CNRS, Université Henri Poincaré, BP 239</s1>
<s2>54506 Vandœuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</inist:fA14>
</affiliation>
</author>
</analytic>
<series><title level="j" type="main">Lecture notes in computer science</title>
<idno type="ISSN">0302-9743</idno>
<imprint><date when="1998">1998</date>
</imprint>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt><title level="j" type="main">Lecture notes in computer science</title>
<idno type="ISSN">0302-9743</idno>
</seriesStmt>
</fileDesc>
<profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Computer system</term>
<term>Formal verification</term>
<term>Parallel system</term>
<term>System design</term>
<term>System simulation</term>
</keywords>
<keywords scheme="Pascal" xml:lang="fr"><term>Conception système</term>
<term>Système informatique</term>
<term>Système parallèle</term>
<term>Simulation système</term>
<term>Vérification formelle</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">Scientists and engineers have successfully developed much useful sequential code using classical programming languages, such as Fortran, and highly performant computers can help them to model problems whilst improving their results of simulation. However, great skill and care are required to design correct parallel code from sequential code. We focus our work on 3 aspects of producing correct parallel code from sequential code. First, we use a theorem prover, namely PVS, as a practical tool for asserting proof obligations and for stating programs and properties. Secondly, we build an abstraction from some sequential code in order to derive a postcondition. Finally, we characterize the "glueing condition" that will ensure the correctness of the final parallel code. Our method does not need any new notation but reuses proof theoretical notations together with the composition of postconditions with respect to the glueing condition.</div>
</front>
</TEI>
<inist><standard h6="B"><pA><fA01 i1="01" i2="1"><s0>0302-9743</s0>
</fA01>
<fA05><s2>1427</s2>
</fA05>
<fA08 i1="01" i2="1" l="ENG"><s1>An experiment in parallelizing an application using formal methods: Computer aided parallelization</s1>
</fA08>
<fA09 i1="01" i2="1" l="ENG"><s1>CAV '98 : computer aided verification : Vancouver BC, 28 June - 2 July 1998</s1>
</fA09>
<fA11 i1="01" i2="1"><s1>COUTURIER (R.)</s1>
</fA11>
<fA11 i1="02" i2="1"><s1>MERY (D.)</s1>
</fA11>
<fA12 i1="01" i2="1"><s1>HU (Alan J.)</s1>
<s9>ed.</s9>
</fA12>
<fA12 i1="02" i2="1"><s1>VARDI (Moshe Y.)</s1>
<s9>ed.</s9>
</fA12>
<fA14 i1="01"><s1>UMR n°7503 LORIA CNRS, Université Henri Poincaré, BP 239</s1>
<s2>54506 Vandœuvre-lès-Nancy</s2>
<s3>FRA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</fA14>
<fA20><s1>345-356</s1>
</fA20>
<fA21><s1>1998</s1>
</fA21>
<fA23 i1="01"><s0>ENG</s0>
</fA23>
<fA26 i1="01"><s0>3-540-64608-6</s0>
</fA26>
<fA43 i1="01"><s1>INIST</s1>
<s2>16343</s2>
<s5>354000076380680320</s5>
</fA43>
<fA44><s0>0000</s0>
<s1>© 1998 INIST-CNRS. All rights reserved.</s1>
</fA44>
<fA45><s0>15 ref.</s0>
</fA45>
<fA47 i1="01" i2="1"><s0>98-0358260</s0>
</fA47>
<fA60><s1>P</s1>
<s2>C</s2>
</fA60>
<fA61><s0>A</s0>
</fA61>
<fA64 i2="1"><s0>Lecture notes in computer science</s0>
</fA64>
<fA66 i1="01"><s0>DEU</s0>
</fA66>
<fA66 i1="02"><s0>USA</s0>
</fA66>
<fC01 i1="01" l="ENG"><s0>Scientists and engineers have successfully developed much useful sequential code using classical programming languages, such as Fortran, and highly performant computers can help them to model problems whilst improving their results of simulation. However, great skill and care are required to design correct parallel code from sequential code. We focus our work on 3 aspects of producing correct parallel code from sequential code. First, we use a theorem prover, namely PVS, as a practical tool for asserting proof obligations and for stating programs and properties. Secondly, we build an abstraction from some sequential code in order to derive a postcondition. Finally, we characterize the "glueing condition" that will ensure the correctness of the final parallel code. Our method does not need any new notation but reuses proof theoretical notations together with the composition of postconditions with respect to the glueing condition.</s0>
</fC01>
<fC02 i1="01" i2="X"><s0>001D02B04</s0>
</fC02>
<fC03 i1="01" i2="X" l="FRE"><s0>Conception système</s0>
<s5>01</s5>
</fC03>
<fC03 i1="01" i2="X" l="ENG"><s0>System design</s0>
<s5>01</s5>
</fC03>
<fC03 i1="01" i2="X" l="SPA"><s0>Concepción sistema</s0>
<s5>01</s5>
</fC03>
<fC03 i1="02" i2="X" l="FRE"><s0>Système informatique</s0>
<s5>02</s5>
</fC03>
<fC03 i1="02" i2="X" l="ENG"><s0>Computer system</s0>
<s5>02</s5>
</fC03>
<fC03 i1="02" i2="X" l="SPA"><s0>Sistema informático</s0>
<s5>02</s5>
</fC03>
<fC03 i1="03" i2="X" l="FRE"><s0>Système parallèle</s0>
<s5>03</s5>
</fC03>
<fC03 i1="03" i2="X" l="ENG"><s0>Parallel system</s0>
<s5>03</s5>
</fC03>
<fC03 i1="03" i2="X" l="SPA"><s0>Sistema paralelo</s0>
<s5>03</s5>
</fC03>
<fC03 i1="04" i2="X" l="FRE"><s0>Simulation système</s0>
<s5>04</s5>
</fC03>
<fC03 i1="04" i2="X" l="ENG"><s0>System simulation</s0>
<s5>04</s5>
</fC03>
<fC03 i1="04" i2="X" l="SPA"><s0>Simulación sistema</s0>
<s5>04</s5>
</fC03>
<fC03 i1="05" i2="3" l="FRE"><s0>Vérification formelle</s0>
<s5>05</s5>
</fC03>
<fC03 i1="05" i2="3" l="ENG"><s0>Formal verification</s0>
<s5>05</s5>
</fC03>
<fN21><s1>243</s1>
</fN21>
</pA>
<pR><fA30 i1="01" i2="1" l="ENG"><s1>International conference on computer aided verification</s1>
<s2>10</s2>
<s3>Vancouver BC CAN</s3>
<s4>1998-06-28</s4>
</fA30>
</pR>
</standard>
<server><NO>PASCAL 98-0358260 INIST</NO>
<ET>An experiment in parallelizing an application using formal methods: Computer aided parallelization</ET>
<AU>COUTURIER (R.); MERY (D.); HU (Alan J.); VARDI (Moshe Y.)</AU>
<AF>UMR n°7503 LORIA CNRS, Université Henri Poincaré, BP 239/54506 Vandœuvre-lès-Nancy/France (1 aut., 2 aut.)</AF>
<DT>Publication en série; Congrès; Niveau analytique</DT>
<SO>Lecture notes in computer science; ISSN 0302-9743; Allemagne; Da. 1998; Vol. 1427; Pp. 345-356; Bibl. 15 ref.</SO>
<LA>Anglais</LA>
<EA>Scientists and engineers have successfully developed much useful sequential code using classical programming languages, such as Fortran, and highly performant computers can help them to model problems whilst improving their results of simulation. However, great skill and care are required to design correct parallel code from sequential code. We focus our work on 3 aspects of producing correct parallel code from sequential code. First, we use a theorem prover, namely PVS, as a practical tool for asserting proof obligations and for stating programs and properties. Secondly, we build an abstraction from some sequential code in order to derive a postcondition. Finally, we characterize the "glueing condition" that will ensure the correctness of the final parallel code. Our method does not need any new notation but reuses proof theoretical notations together with the composition of postconditions with respect to the glueing condition.</EA>
<CC>001D02B04</CC>
<FD>Conception système; Système informatique; Système parallèle; Simulation système; Vérification formelle</FD>
<ED>System design; Computer system; Parallel system; System simulation; Formal verification</ED>
<SD>Concepción sistema; Sistema informático; Sistema paralelo; Simulación sistema</SD>
<LO>INIST-16343.354000076380680320</LO>
<ID>98-0358260</ID>
</server>
</inist>
</record>

Pour manipuler ce document sous Unix (Dilib)

EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/PascalFrancis/Corpus

HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000B97 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/PascalFrancis/Corpus/biblio.hfd -nk 000B97 | SxmlIndent | more

Pour mettre un lien sur cette page dans le réseau Wicri

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    PascalFrancis
   |étape=   Corpus
   |type=    RBID
   |clé=     Pascal:98-0358260
   |texte=   An experiment in parallelizing an application using formal methods: Computer aided parallelization
}}

This area was generated with Dilib version V0.6.33.
Data generation: Mon Jun 10 21:56:28 2019. Site generation: Fri Feb 25 15:29:27 2022

	Serveur d'exploration sur la recherche en informatique en Lorraine
	Attention, ce site est en cours de développement ! Attention, site généré par des moyens informatiques à partir de corpus bruts. Les informations ne sont donc pas validées.

Serveur d'exploration sur la recherche en informatique en Lorraine

An experiment in parallelizing an application using formal methods: Computer aided parallelization

An experiment in parallelizing an application using formal methods: Computer aided parallelization

Source :

Descripteurs français

English descriptors

Abstract

Notice en format standard (ISO 2709)

Format Inist (serveur)

Links to Exploration step

Le document en format XML

Pour manipuler ce document sous Unix (Dilib)

Pour mettre un lien sur cette page dans le réseau Wicri