{"id":664,"date":"2011-10-04T08:54:00","date_gmt":"2011-10-04T08:54:00","guid":{"rendered":"https:\/\/es-wordpress.fbk.eu\/?p=664"},"modified":"2021-05-20T18:32:53","modified_gmt":"2021-05-20T17:32:53","slug":"verification-modulo-theories","status":"publish","type":"post","link":"https:\/\/es.fbk.eu\/index.php\/projects\/verification-modulo-theories\/","title":{"rendered":"Verification Modulo Theories"},"content":{"rendered":"\n<p><strong>Verification Modulo Theories<\/strong> was originally proposed in the <a href=\"https:\/\/sites.google.com\/site\/torino2011ic0901\/programme\" target=\"_blank\" rel=\"noreferrer noopener\">Rich-Model Toolkit&nbsp;meeting<\/a>&nbsp;held in Turin&nbsp;in 2011 (see slides below).<\/p>\n\n\n\n<p>Since then, a format has been defined (see definition of the VMT format in the <a href=\"https:\/\/es.fbk.eu\/tools\/nuxmv\/downloads\/nuxmv-user-manual.pdf\">nuXmv manual<\/a>, page 130), and is now supported by the the nuXmv model checker.&nbsp;<\/p>\n\n\n\n<p>The VMT format is an extension of the <em>SMT-LIBv2<\/em> (SMT2 for short) format to represent symbolic transition systems. VMT exploits the capability offered by the SMT2 language of attaching <em>annotations<\/em> to terms and formulas in order to specify the components of the transition system and the properties to verify.&nbsp;More specifically, the following annotations are used:<\/p>\n\n\n\n<ul class=\"wp-block-list\"><li><strong>:next <em>name<\/em><\/strong> is used to represent state variables. For each variable <em>x<\/em> in the model, the VMT file contains a pair of variables, <em>x<sup>c<\/sup><\/em> and <em>x<sup>n<\/sup><\/em>, representing respectively the current and next version of <em>x<\/em>. The two variables are linked by annotating<em> x<sup>c<\/sup><\/em> with the attribute <em>:next x<sup>n<\/sup><\/em>. All the variables that are not in relation with another by means of a <em>:next<\/em> attribute are considered inputs.<\/li><li><strong>:init true<\/strong> is used to specify the formula for the initial states of the model. This formula should contain neither next-state variables nor input variables. (The \u201cdummy\u201d value <em>true<\/em> in the annotation is needed because the current SMT2 standard requires annotations to always have an associated value.)&nbsp;<\/li><li><strong>:trans true<\/strong> is used to specify the formula for the transition relation.<\/li><li><strong>:invar-property idx<\/strong> is used to specify invariant properties, i.e. formulas of the form <em>Gp<\/em>, where <em>p<\/em> is the formula annotated with <em>:invar-property<\/em>. The non-negative integer <em>idx<\/em> is a unique identifier for the property.<\/li><li><strong>:live-property idx<\/strong> is used to specify an LTL property of the form <em>F Gp<\/em>, where <em>p<\/em> is the formula annotated with <em>:live-property<\/em>. The non-negative integer <em>idx<\/em> is a unique identifier for the property.<\/li><\/ul>\n\n\n\n<p>In a VMT file, only annotated terms and their sub-terms are meaningful. Any other term is ignored. Moreover, only the following commands are allowed to occur in VMT files: <code>set-logic, set-option, declare-sort, define-sort, declare-fun, define-fun<\/code> (For convenience, an additional (<code>assert true<\/code>) command is allowed to appear at the end of the file).<\/p>\n\n\n\n<p>The following example shows a simple NUXMV model and its corresponding VMT translation.<\/p>\n\n\n\n<figure class=\"wp-block-table\"><table><thead><tr><th><strong>NUXMV<\/strong><\/th><th><strong>VMT<\/strong><\/th><\/tr><\/thead><tbody><tr><td><code>-- this is a comment<\/code><\/td><td>&nbsp;<code>; this is a comment<\/code><\/td><\/tr><tr><td><code>MODULE main<\/code><\/td><td>&nbsp;<code>(declare-fun x () Int)<\/code><\/td><\/tr><tr><td><code>VAR x : integer;<\/code><\/td><td>&nbsp;<code>(declare-fun xn () Int)<\/code><\/td><\/tr><tr><td><code>INIT x = 1;<\/code><\/td><td>&nbsp;<code>(define-fun .sv0 () Int (! x :next xn))<\/code><\/td><\/tr><tr><td><code>TRANS next(x) = x + 1;<\/code><\/td><td>&nbsp;\u00a8C11C<\/td><\/tr><tr><td>\u00a8C12C<\/td><td>&nbsp;\u00a8C13C<\/td><\/tr><tr><td>&nbsp;<\/td><td>&nbsp;\u00a8C14C<\/td><\/tr><\/tbody><\/table><\/figure>\n\n\n\n<p>Since the SMT2 format (and thus also the VMT one that inherits from SMT2) does not allow to annnotate the declaration of variables, it is a good practice to insert immediately after the declaration of the variables a set of defines to specify the relations among variables. See for instance the define .sv0 in the example above that introduces the relation between x and xn<\/p>\n\n\n\n<p>In the future, the VMT-LIB initiative will result in a collection of model checking benchmarks for infinite-state transition systems, and in pyVMT, a toolset based on extensions of the\u00a0<a rel=\"noreferrer noopener\" href=\"http:\/\/pysmt.org\" target=\"_blank\">pySMT<\/a>\u00a0library.<\/p>\n\n\n\n<h2 class=\"wp-block-heading\" id=\"h.qryf8yzejwvg\">Format Specification<\/h2>\n\n\n\n<p><a rel=\"noreferrer noopener\" href=\"http:\/\/www.google.com\/url?q=http%3A%2F%2Fes-static.fbk.eu%2Fpeople%2Fgriggio%2Fpapers%2Fvmtlib.pdf&amp;sa=D&amp;sntz=1&amp;usg=AFQjCNG01bu-Yb4b9wc_ArrTnmV39VG1aw\" target=\"_blank\">VMT-LIB Syntax and Semantics Specification, Version 0.1<\/a><\/p>\n\n\n\n<h2 class=\"wp-block-heading\" id=\"h.bz14m2gdcyuy\">Tool Support<\/h2>\n\n\n\n<p><a href=\"http:\/\/www.google.com\/url?q=http%3A%2F%2Fes-static.fbk.eu%2Fpeople%2Fgriggio%2Fic3ia%2Fvmt-tools-latest.tar.gz&amp;sa=D&amp;sntz=1&amp;usg=AFQjCNFqZcOgbrPkXV2SkbSRI1Hr_8XBzg\" target=\"_blank\" rel=\"noreferrer noopener\">vmt-tools<\/a> is a collection of tools for working with the VMT format. Currently, the following tools are provided:<\/p>\n\n\n\n<ul class=\"wp-block-list\"><li><strong>vmt.py<\/strong>: parsing and printing of transition systems in the VMT format.<\/li><li><strong>vmt2btor.py<\/strong>: converter from VMT to the BTOR2 format.<\/li><li><strong>btor2vmt.py<\/strong>: converter from BTOR to VMT.<\/li><li><strong>vmt2horn.py<\/strong>: converter from VMT to Constrained Horn Clauses.<\/li><li><strong>vmt2nuxmv.py<\/strong>: converter from VMT to the SMV dialect of nuXmv.<\/li><li><strong>ltl2vmt.py<\/strong>: a tool to convert a <em>:ltl-property<\/em> into a <em>:live-property<\/em> specification (by compiling them into symbolic tableaux which are then put in product with the transition system).<\/li><\/ul>\n\n\n\n<h2 class=\"wp-block-heading\" id=\"h.o6ide8ubg5x8\">Further converters to VMT<\/h2>\n\n\n\n<ul class=\"wp-block-list\"><li><strong>From Constrained Horn Clauses to VMT<\/strong>: there&#8217;s an horn2vmt tool that comes with the<a rel=\"noreferrer noopener\" href=\"https:\/\/www.google.com\/url?q=https%3A%2F%2Fes-static.fbk.eu%2Fpeople%2Fgriggio%2Fic3ia%2F&amp;sa=D&amp;sntz=1&amp;usg=AFQjCNHvjoRCcMgFZSY_2Yo_9cG6sCN1NA\" target=\"_blank\">IC3ia<\/a> model checker. Alternatively, there is another translator (also called horn2vmt) available on <a rel=\"noreferrer noopener\" href=\"https:\/\/www.google.com\/url?q=https%3A%2F%2Fgithub.com%2Fdbueno%2Fhorn2vmt&amp;sa=D&amp;sntz=1&amp;usg=AFQjCNHEmHpD9EYmhPv2Sd8IyEElBn-cpw\" target=\"_blank\">GitHub<\/a>.<\/li><li><strong>From nuXmv to VMT<\/strong>: the <a rel=\"noreferrer noopener\" href=\"https:\/\/www.google.com\/url?q=https%3A%2F%2Fnuxmv.fbk.eu%2F&amp;sa=D&amp;sntz=1&amp;usg=AFQjCNEmjHbGaxba9AaZbB8YKoNPhSvuaA\" target=\"_blank\">nuXmv<\/a> model checker provides a <em>write_vmt_model<\/em> command.<\/li><li><strong>From Aiger to VMT<\/strong>: via nuXmv.<\/li><li><strong>From VMT to Aiger<\/strong>: via nuXmv.<\/li><\/ul>\n\n\n\n<h2 class=\"wp-block-heading\">Tools Supporting the VMT Format<\/h2>\n\n\n\n<ul class=\"wp-block-list\"><li>The <a href=\"http:\/\/nuxmv.fbk.eu\">nuXmv<\/a> model checker<\/li><li><a href=\"https:\/\/es-static.fbk.eu\/people\/griggio\/ic3ia\/\">IC3ia<\/a>, an open-source implementation of infinite-state IC3 with implicit predicate abstraction<\/li><li><a href=\"https:\/\/github.com\/dbueno\/horn2vmt\">Horn2vmt<\/a>, a tool for translating Horn reachability into transition systems<\/li><li>The <a href=\"https:\/\/github.com\/aman-goel\/avr\">AVR<\/a> model checker<\/li><\/ul>\n\n\n\n<h2 class=\"wp-block-heading\">Benchmarks<\/h2>\n\n\n\n<p>Some transition systems with invariant properties can be found <a href=\"https:\/\/es-static.fbk.eu\/people\/griggio\/papers\/vmt-benchmarks.tar.bz2\">here<\/a>.<\/p>\n\n\n\n<h2 class=\"wp-block-heading\">Presentations<\/h2>\n\n\n\n<h5 class=\"wp-block-heading\">Title:&nbsp;From Satisfiability to Verification Modulo Theories (slides available&nbsp;<a href=\"..\/..\/..\/..\/..\/wp-content\/uploads\/2011\/10\/vmt-lib-discussion.pdf\" data-type=\"URL\" target=\"_blank\" rel=\"noreferrer noopener\">here<\/a>)<br>Speaker:&nbsp;Alessandro Cimatti&nbsp;(FBK, Trento)<br>COST Meeting 2011<\/h5>\n\n\n\n<p><strong>Abstract<\/strong>: The field of Satisfiability Modulo Theories (SMT) has greatly benefited from the SMT-LIB and SMT-COMP initiatives: the definition of a standard language supported the creation of a large collection of benchmarks, and the competition fostered tremendous progress in the performance of SMT solvers. Many practical problems in verification arise from the analysis of the transition systems that can be naturally represented in symbolic form within the SMT framework (e.g. software, timed and hybrid systems, word-level circuits, microcode). However, the SMT initiative does not deal directly with the sequential nature of the transition system, where reachability is defined by unrolling of the transition relation. To draw an analogy with the pure boolean case, SMT is the counterpart of SAT, but there is no &#8220;modulo theory&#8221; counterpart for Model Checking. In fact, many problems in the SMT-LIB are (bounded horizon) verification problems for such transition systems. In this talk I will argue in favour of a Verification Modulo Theory (VMT) initiative. The aim is to define a language, a library of benchmarks, and to set up a competition, for verification problems resulting from transition systems described in SMT. The VMT initiative, while leveraging the advances of SMT, will allow to deal natively with issues resulting from the verification of transition systems, hopefully resulting in a new generation of model checkers modulo theory.<\/p>\n\n\n\n<h5 class=\"wp-block-heading\">Title:&nbsp;VMT techniques (slides available&nbsp;<a href=\"..\/..\/..\/..\/..\/wp-content\/uploads\/2011\/10\/vmt_techniques.pdf\" target=\"_blank\" rel=\"noreferrer noopener\">here<\/a>)<br>Speaker:&nbsp;Stefano Tonetta&nbsp;(FBK, Trento)<br>COST Meeting 2011<\/h5>\n\n\n\n<p><strong>Abstract:<\/strong>&nbsp;Satisfiability-modulo-theory is the problem of checking the satisfiability of a logical formula with a background theory. Many solvers have been optimized for different theories and enhanced with advanced features such as incrementality, unsat cores, interpolation. Meanwhile, many techniques have been conceived to verify properties of transition systems exploiting the efficiency and features of SMT solvers. In fact, by reducing a verification problem to a possibly infinite series of SMT problems, infinite-state systems with reals, integers, or other data types can be verified. This &#8220;Verification-Modulo-Theory&#8221; (VMT) has been applied to different applications such as software, timed and hybrid systems, and microcode. In this talk, we overview some of these techniques including bounded model checking, interpolation-based model checking, k-induction, predicate abstraction, and combination thereof.&nbsp;<\/p>\n","protected":false},"excerpt":{"rendered":"<p>The VMT format is an extension of the SMT-LIBv2 (SMT2 for short) format to represent symbolic transition systems. VMT exploits the capability offered by the SMT2 language of attaching annotations to terms and formulas in order to specify the components of the transition system and the properties to verify.<\/p>\n","protected":false},"author":1,"featured_media":347,"comment_status":"closed","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"_et_pb_use_builder":"off","_et_pb_old_content":"<!-- wp:paragraph -->\n<p><strong>Verification Modulo Theories<\/strong> was originally proposed in the <a href=\"https:\/\/sites.google.com\/site\/torino2011ic0901\/programme\" target=\"_blank\" rel=\"noreferrer noopener\">Rich-Model Toolkit&nbsp;meeting<\/a>&nbsp;held in Turin&nbsp;in 2011 (see slides below).<\/p>\n<!-- \/wp:paragraph -->\n\n<!-- wp:paragraph -->\n<p>Since then, a format has been defined (see definition of the VMT format in the <a href=\"https:\/\/es.fbk.eu\/tools\/nuxmv\/downloads\/nuxmv-user-manual.pdf\">nuXmv manual<\/a>, page 130), and is now supported by the the nuXmv model checker.&nbsp;<\/p>\n<!-- \/wp:paragraph -->\n\n<!-- wp:paragraph -->\n<p>The VMT format is an extension of the <em>SMT-LIBv2<\/em> (SMT2 for short) format to represent symbolic transition systems. VMT exploits the capability offered by the SMT2 language of attaching <em>annotations<\/em> to terms and formulas in order to specify the components of the transition system and the properties to verify.&nbsp;More specifically, the following annotations are used:<\/p>\n<!-- \/wp:paragraph -->\n\n<!-- wp:list -->\n<ul><li><strong>:next <em>name<\/em><\/strong> is used to represent state variables. For each variable <em>x<\/em> in the model, the VMT file contains a pair of variables, <em>x<sup>c<\/sup><\/em> and <em>x<sup>n<\/sup><\/em>, representing respectively the current and next version of <em>x<\/em>. The two variables are linked by annotating<em> x<sup>c<\/sup><\/em> with the attribute <em>:next x<sup>n<\/sup><\/em>. All the variables that are not in relation with another by means of a <em>:next<\/em> attribute are considered inputs.<\/li><li><strong>:init true<\/strong> is used to specify the formula for the initial states of the model. This formula should contain neither next-state variables nor input variables. (The \u201cdummy\u201d value <em>true<\/em> in the annotation is needed because the current SMT2 standard requires annotations to always have an associated value.)&nbsp;<\/li><li><strong>:trans true<\/strong> is used to specify the formula for the transition relation.<\/li><li><strong>:invar-property idx<\/strong> is used to specify invariant properties, i.e. formulas of the form <em>Gp<\/em>, where <em>p<\/em> is the formula annotated with <em>:invar-property<\/em>. The non-negative integer <em>idx<\/em> is a unique identifier for the property.<\/li><li><strong>:live-property idx<\/strong> is used to specify an LTL property of the form <em>F Gp<\/em>, where <em>p<\/em> is the formula annotated with <em>:live-property<\/em>. The non-negative integer <em>idx<\/em> is a unique identifier for the property.<\/li><\/ul>\n<!-- \/wp:list -->\n\n<!-- wp:paragraph -->\n<p>In a VMT file, only annotated terms and their sub-terms are meaningful. Any other term is ignored. Moreover, only the following commands are allowed to occur in VMT files: <code>set-logic, set-option, declare-sort, define-sort, declare-fun, define-fun<\/code> (For convenience, an additional (<code>assert true<\/code>) command is allowed to appear at the end of the file).<\/p>\n<!-- \/wp:paragraph -->\n\n<!-- wp:paragraph -->\n<p>The following example shows a simple NUXMV model and its corresponding VMT translation.<\/p>\n<!-- \/wp:paragraph -->\n\n<!-- wp:table -->\n<figure class=\"wp-block-table\"><table><thead><tr><th><strong>NUXMV<\/strong><\/th><th><strong>VMT<\/strong><\/th><\/tr><\/thead><tbody><tr><td><code>-- this is a comment<\/code><\/td><td>&nbsp;<code>; this is a comment<\/code><\/td><\/tr><tr><td><code>MODULE main<\/code><\/td><td>&nbsp;<code>(declare-fun x () Int)<\/code><\/td><\/tr><tr><td><code>VAR x : integer;<\/code><\/td><td>&nbsp;<code>(declare-fun xn () Int)<\/code><\/td><\/tr><tr><td><code>INIT x = 1;<\/code><\/td><td>&nbsp;<code>(define-fun .sv0 () Int (! x :next xn))<\/code><\/td><\/tr><tr><td><code>TRANS next(x) = x + 1;<\/code><\/td><td>&nbsp;\u00a8C11C<\/td><\/tr><tr><td>\u00a8C12C<\/td><td>&nbsp;\u00a8C13C<\/td><\/tr><tr><td>&nbsp;<\/td><td>&nbsp;\u00a8C14C<\/td><\/tr><\/tbody><\/table><\/figure>\n<!-- \/wp:table -->\n\n<!-- wp:paragraph -->\n<p>Since the SMT2 format (and thus also the VMT one that inherits from SMT2) does not allow to annnotate the declaration of variables, it is a good practice to insert immediately after the declaration of the variables a set of defines to specify the relations among variables. See for instance the define .sv0 in the example above that introduces the relation between x and xn<\/p>\n<!-- \/wp:paragraph -->\n\n<!-- wp:paragraph -->\n<p>In the future, the VMT-LIB initiative will result in a collection of model checking benchmarks for infinite-state transition systems, and in pyVMT, a toolset based on extensions of the&nbsp;<a href=\"http:\/\/pysmt.org\" target=\"_blank\" rel=\"noreferrer noopener\">pySMT<\/a>&nbsp;library.<\/p>\n<!-- \/wp:paragraph -->\n\n<!-- wp:heading -->\n<h2>Tools Supporting the VMT Format<\/h2>\n<!-- \/wp:heading -->\n\n<!-- wp:list -->\n<ul><li>The <a href=\"http:\/\/nuxmv.fbk.eu\">nuXmv<\/a> model checker<\/li><li><a href=\"https:\/\/es-static.fbk.eu\/people\/griggio\/ic3ia\/\">IC3ia<\/a>, an open-source implementation of infinite-state IC3 with implicit predicate abstraction<\/li><li><a href=\"https:\/\/github.com\/dbueno\/horn2vmt\">Horn2vmt<\/a>, a tool for translating Horn reachability into transition systems<\/li><li>The <a href=\"https:\/\/github.com\/aman-goel\/avr\">AVR<\/a> model checker<\/li><\/ul>\n<!-- \/wp:list -->\n\n<!-- wp:heading -->\n<h2>Benchmarks<\/h2>\n<!-- \/wp:heading -->\n\n<!-- wp:paragraph -->\n<p>Some transition systems with invariant properties can be found <a href=\"http:\/\/es-static.fbk.eu\/people\/griggio\/papers\/vmt-benchmarks.tar.bz2\">here<\/a>.<\/p>\n<!-- \/wp:paragraph -->\n\n<!-- wp:heading -->\n<h2>Presentations<\/h2>\n<!-- \/wp:heading -->\n\n<!-- wp:heading {\"level\":4} -->\n<h4>Title:&nbsp;From Satisfiability to Verification Modulo Theories (slides available&nbsp;<a href=\"..\/..\/..\/..\/..\/wp-content\/uploads\/2011\/10\/vmt-lib-discussion.pdf\" data-type=\"URL\" target=\"_blank\" rel=\"noreferrer noopener\">here<\/a>)<br>Speaker:&nbsp;Alessandro Cimatti&nbsp;(FBK, Trento)<br>COST Meeting 2011<\/h4>\n<!-- \/wp:heading -->\n\n<!-- wp:paragraph -->\n<p><strong>Abstract<\/strong>: The field of Satisfiability Modulo Theories (SMT) has greatly benefited from the SMT-LIB and SMT-COMP initiatives: the definition of a standard language supported the creation of a large collection of benchmarks, and the competition fostered tremendous progress in the performance of SMT solvers. Many practical problems in verification arise from the analysis of the transition systems that can be naturally represented in symbolic form within the SMT framework (e.g. software, timed and hybrid systems, word-level circuits, microcode). However, the SMT initiative does not deal directly with the sequential nature of the transition system, where reachability is defined by unrolling of the transition relation. To draw an analogy with the pure boolean case, SMT is the counterpart of SAT, but there is no \"modulo theory\" counterpart for Model Checking. In fact, many problems in the SMT-LIB are (bounded horizon) verification problems for such transition systems. In this talk I will argue in favour of a Verification Modulo Theory (VMT) initiative. The aim is to define a language, a library of benchmarks, and to set up a competition, for verification problems resulting from transition systems described in SMT. The VMT initiative, while leveraging the advances of SMT, will allow to deal natively with issues resulting from the verification of transition systems, hopefully resulting in a new generation of model checkers modulo theory.<\/p>\n<!-- \/wp:paragraph -->\n\n<!-- wp:heading {\"level\":4} -->\n<h4>Title:&nbsp;VMT techniques (slides available&nbsp;<a href=\"..\/..\/..\/..\/..\/wp-content\/uploads\/2011\/10\/vmt_techniques.pdf\" target=\"_blank\" rel=\"noreferrer noopener\">here<\/a>)<br>Speaker:&nbsp;Stefano Tonetta&nbsp;(FBK, Trento)<br>COST Meeting 2011<\/h4>\n<!-- \/wp:heading -->\n\n<!-- wp:paragraph -->\n<p><strong>Abstract:<\/strong>&nbsp;Satisfiability-modulo-theory is the problem of checking the satisfiability of a logical formula with a background theory. Many solvers have been optimized for different theories and enhanced with advanced features such as incrementality, unsat cores, interpolation. Meanwhile, many techniques have been conceived to verify properties of transition systems exploiting the efficiency and features of SMT solvers. In fact, by reducing a verification problem to a possibly infinite series of SMT problems, infinite-state systems with reals, integers, or other data types can be verified. This \"Verification-Modulo-Theory\" (VMT) has been applied to different applications such as software, timed and hybrid systems, and microcode. In this talk, we overview some of these techniques including bounded model checking, interpolation-based model checking, k-induction, predicate abstraction, and combination thereof.&nbsp;<\/p>\n<!-- \/wp:paragraph -->","_et_gb_content_width":"","footnotes":""},"categories":[3],"tags":[],"class_list":["post-664","post","type-post","status-publish","format-standard","has-post-thumbnail","hentry","category-projects","et-has-post-format-content","et_post_format-et-post-format-standard"],"_links":{"self":[{"href":"https:\/\/es.fbk.eu\/index.php\/wp-json\/wp\/v2\/posts\/664","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/es.fbk.eu\/index.php\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/es.fbk.eu\/index.php\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/es.fbk.eu\/index.php\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/es.fbk.eu\/index.php\/wp-json\/wp\/v2\/comments?post=664"}],"version-history":[{"count":26,"href":"https:\/\/es.fbk.eu\/index.php\/wp-json\/wp\/v2\/posts\/664\/revisions"}],"predecessor-version":[{"id":4659,"href":"https:\/\/es.fbk.eu\/index.php\/wp-json\/wp\/v2\/posts\/664\/revisions\/4659"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/es.fbk.eu\/index.php\/wp-json\/wp\/v2\/media\/347"}],"wp:attachment":[{"href":"https:\/\/es.fbk.eu\/index.php\/wp-json\/wp\/v2\/media?parent=664"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/es.fbk.eu\/index.php\/wp-json\/wp\/v2\/categories?post=664"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/es.fbk.eu\/index.php\/wp-json\/wp\/v2\/tags?post=664"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}