Skip to content
Snippets Groups Projects
Commit 443ef2bf authored by Allan Blanchard's avatar Allan Blanchard
Browse files

Resize H3

parent 7ea62207
No related branches found
No related tags found
1 merge request!11publis
This commit is part of merge request !11. Comments created here will be created in the context of that merge request.
...@@ -71,19 +71,9 @@ ...@@ -71,19 +71,9 @@
font-size: 21px; font-size: 21px;
} }
} }
@media (min-width: 1024px) {
.defaultPage h3 {
font-size: 25px;
}
}
@media (min-width: 1600px) { @media (min-width: 1600px) {
.defaultPage h3 { .defaultPage h3 {
font-size: 28px; font-size: 24px;
}
}
@media (min-width: 1890px) {
.defaultPage h3 {
font-size: 30px;
} }
} }
.defaultPage article { .defaultPage article {
......
...@@ -215,7 +215,7 @@ This page is dedicated to publications related to Frama-C. It is not exhaustive, ...@@ -215,7 +215,7 @@ This page is dedicated to publications related to Frama-C. It is not exhaustive,
<http://julien.signoles.free.fr/publis/2017_rvcubes_tool.pdf>\ <http://julien.signoles.free.fr/publis/2017_rvcubes_tool.pdf>\
*An overview of the E-ACSL plug-in.* *An overview of the E-ACSL plug-in.*
- Kostyantyn Vorobyov, Julien Signoles, and Nikolai Kosmatov.\ - Kostyantyn Vorobyov, Julien Signoles, and Nikolai Kosmatov.\
Shadow state encoding for efficient monitoring of block-level properties.\ **Shadow state encoding for efficient monitoring of block-level properties.**\
In International Symposium on Memory Management (ISMM), June 2017.\ In International Symposium on Memory Management (ISMM), June 2017.\
<http://julien.signoles.free.fr/publis/2017_ismm.pdf>\ <http://julien.signoles.free.fr/publis/2017_ismm.pdf>\
*Presentation of the shadow memory technique used by E-ACSL to monitor *Presentation of the shadow memory technique used by E-ACSL to monitor
...@@ -279,7 +279,7 @@ This page is dedicated to publications related to Frama-C. It is not exhaustive, ...@@ -279,7 +279,7 @@ This page is dedicated to publications related to Frama-C. It is not exhaustive,
# Internal Plug-ins at CEA # Internal Plug-ins at CEA
## Cfp ### Cfp
#### Founding Articles #### Founding Articles
...@@ -289,7 +289,7 @@ This page is dedicated to publications related to Frama-C. It is not exhaustive, ...@@ -289,7 +289,7 @@ This page is dedicated to publications related to Frama-C. It is not exhaustive,
<http://julien.signoles.free.fr/publis/2017_lopstr.pdf>\ <http://julien.signoles.free.fr/publis/2017_lopstr.pdf>\
Best paper award. Best paper award.
## MetACSL ### MetACSL
#### Founding Articles #### Founding Articles
...@@ -299,7 +299,7 @@ This page is dedicated to publications related to Frama-C. It is not exhaustive, ...@@ -299,7 +299,7 @@ This page is dedicated to publications related to Frama-C. It is not exhaustive,
In International Conference on Tools and Algorithms for the Construction In International Conference on Tools and Algorithms for the Construction
and Analysis of Systems (TACAS), April 2019. and Analysis of Systems (TACAS), April 2019.
## PathCrawler ### PathCrawler
##### Manual ##### Manual
...@@ -401,7 +401,7 @@ This page is dedicated to publications related to Frama-C. It is not exhaustive, ...@@ -401,7 +401,7 @@ This page is dedicated to publications related to Frama-C. It is not exhaustive,
The final publication is available from IEEE.\ The final publication is available from IEEE.\
<http://dx.doi.org/10.1109/ICSTW.2011.85> <http://dx.doi.org/10.1109/ICSTW.2011.85>
## SecureFlow ### SecureFlow
##### Thesis ##### Thesis
...@@ -430,7 +430,7 @@ available from the official Frama-C website (<http://frama-c.com>). ...@@ -430,7 +430,7 @@ available from the official Frama-C website (<http://frama-c.com>).
These plug-ins may be either closed or open source. These plug-ins may be either closed or open source.
## Jessie ### Jessie
#### Manual #### Manual
...@@ -631,8 +631,7 @@ These plug-ins may be either closed or open source. ...@@ -631,8 +631,7 @@ These plug-ins may be either closed or open source.
In NASA Formal Methods 2013.\ In NASA Formal Methods 2013.\
*Usually, proofs involving numerical computations are conducted in the infinitely precise realm of the field of real numbers. However, numerical computations in these algorithms are often implemented using floating point numbers. The use of a finite representation of real numbers introduces uncertainties as to whether the properties verified in the theoretical setting hold in practice. This short paper describes work in progress aimed at addressing these concerns. Given a formally proven algorithm, written in the Program Verification System(PVS), the Frama-C suite of tools is used to identify sufficient conditions and verify that under such conditions the rounding errors arising in a C implementation of the algorithm do not affect its correctness. The technique is illustrated using an algorithm for detecting loss of separation among aircraft.* *Usually, proofs involving numerical computations are conducted in the infinitely precise realm of the field of real numbers. However, numerical computations in these algorithms are often implemented using floating point numbers. The use of a finite representation of real numbers introduces uncertainties as to whether the properties verified in the theoretical setting hold in practice. This short paper describes work in progress aimed at addressing these concerns. Given a formally proven algorithm, written in the Program Verification System(PVS), the Frama-C suite of tools is used to identify sufficient conditions and verify that under such conditions the rounding errors arising in a C implementation of the algorithm do not affect its correctness. The technique is illustrated using an algorithm for detecting loss of separation among aircraft.*
### Cost
## Cost
- Nicolas Ayache, Roberto M. Amadio and Yann Régis-Gianas.\ - Nicolas Ayache, Roberto M. Amadio and Yann Régis-Gianas.\
**Certifying and reasoning on cost annotations in C programs.**\ **Certifying and reasoning on cost annotations in C programs.**\
...@@ -652,7 +651,7 @@ These plug-ins may be either closed or open source. ...@@ -652,7 +651,7 @@ These plug-ins may be either closed or open source.
by a compiler for the synchronous programming language Lustre used by a compiler for the synchronous programming language Lustre used
in critical embedded software.* in critical embedded software.*
## Fan-C ### Fan-C
- Pascal Cuoq, David Delmas, Stéphane Duprat and Victoria Moya - Pascal Cuoq, David Delmas, Stéphane Duprat and Victoria Moya
Lamiel.\ Lamiel.\
...@@ -661,7 +660,7 @@ These plug-ins may be either closed or open source. ...@@ -661,7 +660,7 @@ These plug-ins may be either closed or open source.
(ERTS'12).\ (ERTS'12).\
<http://www.erts2012.org/Site/0P2RUC89/5C-3.pdf> <http://www.erts2012.org/Site/0P2RUC89/5C-3.pdf>
## SANTE ### SANTE
- Omar Chebaro, Nikolaï Kosmatov, Alain Giorgetti and Jacques - Omar Chebaro, Nikolaï Kosmatov, Alain Giorgetti and Jacques
Julliand.\ Julliand.\
...@@ -721,7 +720,7 @@ These plug-ins may be either closed or open source. ...@@ -721,7 +720,7 @@ These plug-ins may be either closed or open source.
dynamic analysis. Moreover, simplifying the program makes it easier dynamic analysis. Moreover, simplifying the program makes it easier
to analyze detected errors and remaining alarms. To appear.* to analyze detected errors and remaining alarms. To appear.*
## SIDAN ### SIDAN
- Jonathan-Christopher Demay, Éric Totel and Frédéric Tronel.\ - Jonathan-Christopher Demay, Éric Totel and Frédéric Tronel.\
**SIDAN: a tool dedicated to Software Instrumentation for Detecting **SIDAN: a tool dedicated to Software Instrumentation for Detecting
...@@ -729,7 +728,7 @@ These plug-ins may be either closed or open source. ...@@ -729,7 +728,7 @@ These plug-ins may be either closed or open source.
4th International Conference on Risks and Security of Internet and 4th International Conference on Risks and Security of Internet and
Systems (CRISIS'2009), October 2009. Systems (CRISIS'2009), October 2009.
## STAC ### STAC
- Dumitru Ceara, Laurent Mounier and Marie-Laure Potet.\ - Dumitru Ceara, Laurent Mounier and Marie-Laure Potet.\
**Taint Dependency Sequences: a characterization of insecure **Taint Dependency Sequences: a characterization of insecure
...@@ -737,7 +736,7 @@ These plug-ins may be either closed or open source. ...@@ -737,7 +736,7 @@ These plug-ins may be either closed or open source.
Modeling and Detecting Vulnerabilities workshop (MDV'10), associated Modeling and Detecting Vulnerabilities workshop (MDV'10), associated
to ICST 2010, April 2010. to ICST 2010, April 2010.
## Taster ### Taster
- David Delmas, Stéphane Duprat, Victoria Moya Lamiel and Julien - David Delmas, Stéphane Duprat, Victoria Moya Lamiel and Julien
Signoles.\ Signoles.\
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment