Changeset 57 for papers/FDL2012
- Timestamp:
- Mar 9, 2012, 3:31:35 PM (13 years ago)
- Location:
- papers/FDL2012
- Files:
-
- 3 edited
Legend:
- Unmodified
- Added
- Removed
-
papers/FDL2012/abstraction_refinement.tex
r56 r57 47 47 \item $\sigma$ is not a path of the concrete system $M$: $\exists k$ such 48 48 that $(s_{k}, s_{k+1}) \not\in R$. 49 \end{itemize} 49 50 \end{definition} 50 51 -
papers/FDL2012/framework.tex
r56 r57 114 114 115 115 As the abstract model $\widehat{M}$ is generated from the conjunction of verified properties of the components in the concrete model $M$, it can be seen as the composition of the AKS of each property. 116 The AKS composition has been defined in \cite{ these_braunstein}; it extends116 The AKS composition has been defined in \cite{braunstein_phd07}; it extends 117 117 the classical synchrounous composition of Moore machine to deal with 118 118 four-valued variables. -
papers/FDL2012/myBib.bib
r48 r57 43 43 author = "E. M. Clarke and O. Grumberg and S. Jha and Y. Lu and H. Veith", 44 44 title = "{Counterexample-guided Abstraction Refinement}", 45 booktitle = "Computer Aided Verification (CAV 45 booktitle = "Computer Aided Verification (CAV'00)", 46 46 address = "Chicago, IL", 47 47 year = 2000, … … 86 86 author = "H. S. Jin and M. Awedh and F. Somenzi", 87 87 title = "{CirCUs: A Satisfiablilty Solver Geared Towards Bounded Model Checking}", 88 booktitle = {16th Conference on Computer Aided Verification (CAV 88 booktitle = {16th Conference on Computer Aided Verification (CAV'04)}, 89 89 pages = {519-522}, 90 90 year = 2004, … … 111 111 @article{ bara08abs_composant, 112 112 author = "A. Bara", 113 title = "{Abstraction de Composant pour la Và ©rification par Model-Checking}",114 journal = {Mà ©moire de DiplÃŽme Universitaire OMP - LIP6-SOC},113 title = "{Abstraction de Composant pour la Vérification par Model-Checking}", 114 journal = {Mémoire de DiplÃÂŽme Universitaire OMP - LIP6-SOC}, 115 115 year = 2008 116 116 } … … 143 143 author = "H. Peng and Y. Mokhtari and S. Tahar ", 144 144 title = "{Environment Synthesis for Compositional Model Checking} ", 145 booktitle = "In ICCD â02 : Proceedings of the 20th International Conference on Computer Design",145 booktitle = "In ICCD'02 : Proceedings of the 20th International Conference on Computer Design", 146 146 pages = {70-75}, 147 147 address = "Freiburg, Germany", … … 154 154 author = "M. Schickel and V. Nimbler and M. Braun and H. Eveking ", 155 155 title = "{On Consistency and Completeness of Property-Sets: Exploiting the Property-Based Design Process} ", 156 booktitle = "In FDL â06: Proceedings of Forum on specification and Design Languages",156 booktitle = "In FDL'06: Proceedings of Forum on specification and Design Languages", 157 157 year = 2006 158 158 } … … 160 160 161 161 @conference{ CiardoLS00mdd_async, 162 author = "G.Ciardo and G. Là Œttgen and R. Siminiceanu",162 author = "G.Ciardo and G. LÃÂŒttgen and R. Siminiceanu", 163 163 title = "{ Efficient symbolic state-space construction for asynchronous systems} ", 164 164 booktitle = "In Proc. of ICATPN '2000", … … 184 184 author = "T. A. Henzinger and S. Qadeer and S. K. Rajamani", 185 185 title = "{ You Assume, We Guarantee : Methodology and Case Studies} ", 186 booktitle = "CAV â98 : Proceedings of the 10th International Conference on Computer Aided Verification",186 booktitle = "CAV'98 : Proceedings of the 10th International Conference on Computer Aided Verification", 187 187 volume = 1427, 188 188 pages = {440-451}, … … 205 205 206 206 @conference{ GrafSaidi97abstract_construct, 207 author = " S. Graf and H. Saà ¯di",207 author = " S. Graf and H. Saïdi", 208 208 title = "{ Construction of Abstract State Graphs with PVS} ", 209 booktitle = " In CAV â97: Proceedings of the 9th International Conference on Computer Aided Verification",209 booktitle = " In CAV'97: Proceedings of the 9th International Conference on Computer Aided Verification", 210 210 volume = 1254, 211 211 year = 1997, … … 290 290 } 291 291 292 @PHDTHESIS{braunstein_phd07, 293 author = {C.~Braunstein}, 294 title = {"Conception Incrémentale, Vérification de Composants Matériels et 295 Méthode d'abstraction pour la Vérification de SystÚmes Intégrés sur 296 Puce"}, 297 school = {{Universitée Pierre et Marie Curie (Paris 6)}}, 298 year = {2007}, 299 address = {LIP6/SOC}, 300 owner = {cecile}, 301 timestamp = {2007.04.16} 302 } 292 303 293 304 @misc{ patanshnik88bibtex,
Note: See TracChangeset
for help on using the changeset viewer.